Proof of proveit.core_expr_types.conditionals.implication_from_conditional theorem

import proveit
from proveit import Conditional
from proveit import A, Q
from proveit.logic import TRUE, Equals
theory = proveit.Theory() # the theorem's theory

%proving implication_from_conditional

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

Q_eq_T = Equals(Q, TRUE).prove(assumptions=[Q])

Q_eq_T:  ⊢  

Q_eq_T.sub_right_side_into(Conditional(A, Q), 
                           assumptions=[Conditional(A, Q)]).simplify()

,  ⊢  

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

%qed

proveit.core_expr_types.conditionals.implication_from_conditional has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	⊢
2	instantiation	3, 4, 5	,  ⊢
	: , :
3	theorem		⊢
	proveit.logic.equality.rhs_via_equality
4	instantiation	6, 7, 8	,  ⊢
	: , :
5	instantiation	9	⊢
	:
6	theorem		⊢
	proveit.logic.equality.substitute_in_true
7	assumption		⊢
8	assumption		⊢
9	axiom		⊢
	proveit.core_expr_types.conditionals.true_condition_reduction