Proof of proveit.logic.booleans.conjunction.falsified_and_if_neither theorem

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.conjunction import nand_if_neither
theory = proveit.Theory() # the theorem's theory

%proving falsified_and_if_neither

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
falsified_and_if_neither:
(see dependencies)

falsified_and_if_neither may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

defaults.assumptions = falsified_and_if_neither.all_conditions()

defaults.assumptions:

nand_if_neither

 ⊢  

nand = nand_if_neither.instantiate({A:A, B:B})

nand: ,  ⊢  

# To do this manually, we'd execute nand.equate_negated_to_false(assumptions=conditions) and then generalize.
# But it can figure this out via automation.
%qed

proveit.logic.booleans.conjunction.falsified_and_if_neither has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	,  ⊢
	:
2	axiom		⊢
	proveit.logic.booleans.negation.negation_elim
3	instantiation	4, 5, 6	,  ⊢
	: , :
4	theorem		⊢
	proveit.logic.booleans.conjunction.nand_if_neither
5	assumption		⊢
6	assumption		⊢