→对→左置换
theorem iilp (A B C: wff): $ (A \imp B \imp C) \imp B \imp A \imp C $;
Step | Hyp | Ref | Expression |
---|---|---|---|
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 |