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

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

%proving iff_implies_right

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

iff_def

 ⊢  

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

iff_def_spec:  ⊢  

iff_def_spec.derive_right_via_equality(
    assumptions=iff_implies_right.conditions).derive_left()

 ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.booleans.conjunction.left_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