→对→右插入
theorem imp_for_imp_right_insert (A B C: wff): $ ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mp_imp_left_intro | (((A \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp B \imp A \imp B) \imp (A \imp C) \imp B \imp C) \imp (((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (((A \imp B) \imp C) \imp (A \imp C) \imp B \imp A \imp B) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |
|
| 2 | mp_imp_left_intro | (((B \imp A \imp B) \imp B \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp B \imp A \imp B) \imp (A \imp C) \imp B \imp C |
|
| 3 | mp_curried | ((B \imp A \imp B) \imp B \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 4 | 2, 3 | mp | ((A \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp B \imp A \imp B) \imp (A \imp C) \imp B \imp C |
| 5 | 1, 4 | mp | (((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (((A \imp B) \imp C) \imp (A \imp C) \imp B \imp A \imp B) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |
| 6 | mp_imp_left_intro | (((A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp
((A \imp C) \imp B \imp (A \imp B) \imp C) \imp
(A \imp C) \imp
(B \imp A \imp B) \imp
B \imp
C) \imp
(((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp
(((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C) \imp
((A \imp B) \imp C) \imp
(A \imp C) \imp
(B \imp A \imp B) \imp
B \imp
C |
|
| 7 | mp_imp_left_intro | (((B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp B \imp (A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 8 | mp_curried | ((B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 9 | 7, 8 | mp | ((A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp C) \imp B \imp (A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 10 | 6, 9 | mp | (((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 11 | imp_left_intro | ((A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 12 | imp_left_intro | ((B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C) \imp (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 13 | imp_for_imp_left_insert | (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
|
| 14 | 12, 13 | mp | (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 15 | 11, 14 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp (A \imp B) \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 16 | 10, 15 | mp | (((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 17 | mp_imp_left_intro | (((A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp C) \imp (A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C) \imp (((A \imp B) \imp C) \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 (A \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
|
| 18 | mp_imp_left_intro | ((((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp C) \imp (A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
|
| 19 | mp_curried | (((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
|
| 20 | 18, 19 | mp | ((A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp C) \imp (A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
| 21 | 17, 20 | mp | (((A \imp B) \imp C) \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 (A \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
| 22 | imp_left_intro | ((A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
|
| 23 | imp_left_intro | (((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C) \imp (A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
|
| 24 | imp_left_intro | ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
|
| 25 | 23, 24 | mp | (A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
| 26 | 22, 25 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp ((A \imp B) \imp C) \imp B \imp (A \imp B) \imp C |
| 27 | 21, 26 | mp | (((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
| 28 | imp_for_imp_left_intro | (((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C) \imp (((A \imp B) \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C |
|
| 29 | imp_for_imp_right_left_intro | (((A \imp B) \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C |
|
| 30 | imp_reflect | ((A \imp B) \imp C) \imp (A \imp B) \imp C |
|
| 31 | 29, 30 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C |
| 32 | 28, 31 | mp | (((A \imp B) \imp C) \imp (A \imp B) \imp C) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C |
| 33 | 32, 30 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp (A \imp B) \imp C |
| 34 | 27, 33 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp (A \imp B) \imp C |
| 35 | 16, 34 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp (B \imp A \imp B) \imp B \imp C |
| 36 | 5, 35 | mp | (((A \imp B) \imp C) \imp (A \imp C) \imp B \imp A \imp B) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |
| 37 | imp_left_intro | ((A \imp C) \imp B \imp A \imp B) \imp ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp A \imp B |
|
| 38 | imp_left_intro | (B \imp A \imp B) \imp (A \imp C) \imp B \imp A \imp B |
|
| 39 | imp_left_intro | B \imp A \imp B |
|
| 40 | 38, 39 | mp | (A \imp C) \imp B \imp A \imp B |
| 41 | 37, 40 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp A \imp B |
| 42 | 36, 41 | mp | ((A \imp B) \imp C) \imp (A \imp C) \imp B \imp C |