Theorem imp_imp_elimrsl ≪ | index | src | ≫

\imp右侧左消除

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

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

Axiom use

Logic (ax_mp, ax_1, ax_2)