Proof of proveit.logic.booleans.implication.falsified_antecedent_implication theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import A, B
from proveit.logic import TRUE, in_bool, Not, Equals

%proving falsified_antecedent_implication

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

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

contradiction = Not(A).derive_contradiction(assumptions=[A, Not(A)])

contradiction: ,  ⊢  

not_b_contradiction = contradiction.as_implication(Not(Equals(B, TRUE)))

not_b_contradiction: ,  ⊢  

BeqT_via_contradiction = not_b_contradiction.derive_via_contradiction()

BeqT_via_contradiction: ,  ⊢  

B_via_contradiction = B.prove(assumptions=[A, Not(A)])

B_via_contradiction: ,  ⊢  

B_via_contradiction.as_implication(A)

 ⊢  

%qed

proveit.logic.booleans.implication.falsified_antecedent_implication has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	instantiation	3, 4	,  ⊢
	:
3	axiom		⊢
	proveit.logic.booleans.eq_true_elim
4	instantiation	5, 6, 7	,  ⊢
	:
5	axiom		⊢
	proveit.logic.booleans.implication.affirmation_via_contradiction
6	instantiation	8	⊢
	: , :
7	deduction	9	,  ⊢
8	axiom		⊢
	proveit.logic.equality.equality_in_bool
9	instantiation	10, 11, 12	,  ⊢
	:
10	theorem		⊢
	proveit.logic.booleans.negation.negation_contradiction
11	assumption		⊢
12	assumption		⊢