Theorem imp_tran ≪ | index | src | ≫

\imp传递

theorem imp_tran (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;

Step	Hyp	Ref	Expression
1		imp_introrevr_imp	(A \imp B) \imp (B \imp C) \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)