Theorem imp_trans_curried ≪ | index | src | ≫

→传递（柯里化形式）

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

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

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)