Theorem iilp | index | src |

→对→左置换

theorem iilp (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;
StepHypRefExpression
1 iili
((B \imp A \imp B \imp C) \imp B \imp A \imp C) \imp ((A \imp B \imp C) \imp B \imp A \imp B \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
2 iils
(B \imp (A \imp B \imp C) \imp A \imp C) \imp (B \imp A \imp B \imp C) \imp B \imp A \imp C
3 iili
((A \imp B) \imp (A \imp B \imp C) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp (A \imp B \imp C) \imp A \imp C
4 iili
(((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C) \imp
  ((A \imp B) \imp (A \imp B \imp C) \imp A \imp B) \imp
  (A \imp B) \imp
  (A \imp B \imp C) \imp
  A \imp
  C
5 iils
((A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp ((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C
6 iils
(A \imp B \imp C) \imp (A \imp B) \imp A \imp C
7 5, 6 mp
((A \imp B \imp C) \imp A \imp B) \imp (A \imp B \imp C) \imp A \imp C
8 4, 7 mp
((A \imp B) \imp (A \imp B \imp C) \imp A \imp B) \imp (A \imp B) \imp (A \imp B \imp C) \imp A \imp C
9 ili
(A \imp B) \imp (A \imp B \imp C) \imp A \imp B
10 8, 9 mp
(A \imp B) \imp (A \imp B \imp C) \imp A \imp C
11 3, 10 mp
(B \imp A \imp B) \imp B \imp (A \imp B \imp C) \imp A \imp C
12 ili
B \imp A \imp B
13 11, 12 mp
B \imp (A \imp B \imp C) \imp A \imp C
14 2, 13 mp
(B \imp A \imp B \imp C) \imp B \imp A \imp C
15 1, 14 mp
((A \imp B \imp C) \imp B \imp A \imp B \imp C) \imp (A \imp B \imp C) \imp B \imp A \imp C
16 ili
(A \imp B \imp C) \imp B \imp A \imp B \imp C
17 15, 16 mp
(A \imp B \imp C) \imp B \imp A \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)