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

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

%proving untrue_antecedent_implication

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

defaults.assumptions = (A, NotEquals(A, TRUE))

defaults.assumptions:

contradiction = NotEquals(A, TRUE).derive_contradiction()

contradiction: ,  ⊢  

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

not_b_contradiction: ,  ⊢  

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

BeqT_via_contradiction = not_b_contradiction.derive_via_contradiction()

BeqT_via_contradiction: ,  ⊢  

B_via_contradiction = B.prove()

B_via_contradiction: ,  ⊢  

B_via_contradiction.as_implication(A)

 ⊢  

%qed

proveit.logic.booleans.implication.untrue_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.equality.not_equals_contradiction
11	instantiation	13, 14	⊢
	:
12	assumption		⊢
13	axiom		⊢
	proveit.logic.booleans.eq_true_intro
14	assumption		⊢