Theorem imp_imp_swapl ≪ | index | src | ≫

\imp\imp左交换

theorem imp_imp_swapl (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;
StepHypRefExpression
1 imp_introl_imp 
(((A \imp B) \imp A \imp C) \imp B \imp A \imp C) \imp ((A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
2 imp_imp_insl 
(((A \imp B) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp B \imp A \imp B) \imp
  ((A \imp B) \imp A \imp C) \imp
  B \imp
  A \imp
  C
3 imp_introl_imp 
((A \imp B) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp A \imp C
4 2, 3 ax_mp 
(((A \imp B) \imp A \imp C) \imp B \imp A \imp B) \imp ((A \imp B) \imp A \imp C) \imp B \imp A \imp C
5 introl_imp 
(B \imp A \imp B) \imp ((A \imp B) \imp A \imp C) \imp B \imp A \imp B
6 introl_imp 
B \imp A \imp B
7 5, 6 ax_mp 
((A \imp B) \imp A \imp C) \imp B \imp A \imp B
8 4, 7 ax_mp 
((A \imp B) \imp A \imp C) \imp B \imp A \imp C
9 1, 8 ax_mp 
((A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
10 imp_imp_insl 
(A \imp B \imp C) \imp (A \imp B) \imp A \imp C
11 9, 10 ax_mp 
(A \imp B \imp C) \imp B \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)