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

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

%proving nand_if_not_right

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

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

defaults.assumptions = nand_if_not_right.conditions

defaults.assumptions:

nand_if_left_but_not_right.instantiate({A:TRUE}, auto_simplify=False)

 ⊢  

nand_if_neither.instantiate({A:FALSE}, auto_simplify=False)

 ⊢  

nand_if_not_right.conclude_by_cases()

 ⊢  

%qed

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

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3, 4, 5*	⊢
	: , : , : , : , : , : , :
2	instantiation	6, 7, 8	⊢
	: , :
3	conjecture		⊢
	proveit.logic.booleans.quantification.universality.bundle
4	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
5	instantiation	9, 10, 11	⊢
	: , : , : , :
6	conjecture		⊢
	proveit.logic.booleans.forall_over_bool_by_cases
7	generalization	12	⊢
8	generalization	13	⊢
9	conjecture		⊢
	proveit.core_expr_types.conditionals.condition_prepend_reduction
10	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
11	instantiation	14	⊢
	: , :
12	instantiation	15, 16, 19	⊢
	: , :
13	instantiation	17, 18, 19	⊢
	: , :
14	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
15	theorem		⊢
	proveit.logic.booleans.conjunction.nand_if_left_but_not_right
16	axiom		⊢
	proveit.logic.booleans.true_axiom
17	theorem		⊢
	proveit.logic.booleans.conjunction.nand_if_neither
18	theorem		⊢
	proveit.logic.booleans.negation.not_false
19	assumption		⊢
*equality replacement requirements