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

import proveit
from proveit import defaults
from proveit import A
theory = proveit.Theory() # the theorem's theory

%proving from_contraposition

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

defaults.assumptions = list(from_contraposition.all_conditions()) + [A]

defaults.assumptions:

not_b_implies_not_a = defaults.assumptions[0]

not_b_implies_not_a:

not_b_implies_not_a.deny_antecedent().as_implication(A)

,  ⊢  

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

%qed # automation can take it from here

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

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	,  ⊢
2	instantiation	3, 4, 5, 6	, ,  ⊢
	: , :
3	theorem		⊢
	proveit.logic.booleans.implication.modus_tollens_affirmation
4	assumption		⊢
5	assumption		⊢
6	instantiation	7, 8	⊢
	:
7	theorem		⊢
	proveit.logic.booleans.negation.double_negation_intro
8	assumption		⊢