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

import proveit
from proveit.logic import Implies
from proveit import A, B, C
theory = proveit.Theory() # the theorem's theory

%proving implication_transitivity

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

Implies(A, C).prove(assumptions=[Implies(A, B), Implies(B, C)])

,  ⊢  

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

%qed # done solely via automation

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

	step type	requirements	statement
0	generalization	1	⊢
1	deduction	2	,  ⊢
2	modus ponens	3, 4	, ,  ⊢
3	assumption		⊢
4	modus ponens	5, 6	,  ⊢
5	assumption		⊢
6	assumption		⊢