Theorem imp_introrevr_imp ≪ | index | src | ≫

\imp对\imp右逆引入

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

Step	Hyp	Ref	Expression
1		imp_imp_swapl	((B \imp C) \imp (A \imp B) \imp A \imp C) \imp (A \imp B) \imp (B \imp C) \imp A \imp C
2		imp_introl_imp	(B \imp C) \imp (A \imp B) \imp A \imp C
3	1, 2	ax_mp	(A \imp B) \imp (B \imp C) \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)