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

import proveit
from proveit.logic.booleans.implication  import iff_def
from proveit import A, B
theory = proveit.Theory() # the theorem's theory

%proving iff_implies_left

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

iff_def

 ⊢  

iff_def_spec = iff_def.instantiate({A:A, B:B})

iff_def_spec:  ⊢  

iff_unfolded = iff_def_spec.derive_right_via_equality(
    assumptions=iff_implies_left.conditions)

iff_unfolded:  ⊢  

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

iff_unfolded.derive_right()

 ⊢  

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
3	instantiation	4, 5, 6	⊢
	: , :
4	theorem		⊢
	proveit.logic.equality.rhs_via_equality
5	assumption		⊢
6	instantiation	7	⊢
	: , :
7	axiom		⊢
	proveit.logic.booleans.implication.iff_def