Theorem imp_for_imp_right_left_intro ≪ | index | src | ≫

→对→右左引入

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

Step	Hyp	Ref	Expression
1		imp_for_imp_left_intro	(B \imp C \imp B) \imp (A \imp B) \imp A \imp C \imp B
2		imp_left_intro	B \imp C \imp B
3	1, 2	mp	(A \imp B) \imp A \imp C \imp B

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)