Theorem imp_for_imp_left_insert ≪ | index | src | ≫

→对→左插入

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

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

Axiom use

ZFC (ax_p2)