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

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

%proving false_antecedent_implication

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

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

Prove $A$ assuming $\bot$ via deriving a contradiction.

F_assuming_F = FALSE.prove(assumptions=[FALSE])

F_assuming_F:  ⊢  

not_a_impl_F = F_assuming_F.as_implication(Not(A))

not_a_impl_F:  ⊢  

A_via_contradiction = not_a_impl_F.derive_via_contradiction(assumptions=[in_bool(A)])

A_via_contradiction: ,  ⊢  

Now we can derive $\bot \Rightarrow A$ via Deduction.

A_via_contradiction.as_implication(FALSE)

 ⊢  

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	instantiation	3, 4, 5	,  ⊢
	:
3	axiom		⊢
	proveit.logic.booleans.implication.affirmation_via_contradiction
4	assumption		⊢
5	deduction	6	⊢
6	assumption		⊢