Theorem imp_for_imp_left_extract ≪ | index | src | ≫

→对→左提取

theorem imp_for_imp_left_extract (A B C: wff):
  $ ((A \imp B) \imp A \imp C) \imp A \imp B \imp C $;
StepHypRefExpression
1 mp_imp_left_intro 
((A \imp B \imp A \imp C) \imp (A \imp B \imp A) \imp A \imp B \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp A) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  C
2 mp_imp_left_intro 
((B \imp A \imp C) \imp (B \imp A) \imp B \imp C) \imp (A \imp B \imp A \imp C) \imp (A \imp B \imp A) \imp A \imp B \imp C
3 mp_imp_left_intro 
((A \imp C) \imp A \imp C) \imp (B \imp A \imp C) \imp (B \imp A) \imp B \imp C
4 mp_curried 
(A \imp C) \imp A \imp C
5 3, 4 mp 
(B \imp A \imp C) \imp (B \imp A) \imp B \imp C
6 2, 5 mp 
(A \imp B \imp A \imp C) \imp (A \imp B \imp A) \imp A \imp B \imp C
7 1, 6 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp A) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  C
8 mp_imp_left_intro 
((A \imp B \imp (A \imp B) \imp A \imp C) \imp (A \imp B \imp A \imp B) \imp A \imp B \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp B) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  A \imp
  C
9 mp_imp_left_intro 
((B \imp (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 B) \imp A \imp C) \imp
  (A \imp B \imp A \imp B) \imp
  A \imp
  B \imp
  A \imp
  C
10 mp_imp_left_intro 
(((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C) \imp (B \imp (A \imp B) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp A \imp C
11 mp_curried 
((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C
12 10, 11 mp 
(B \imp (A \imp B) \imp A \imp C) \imp (B \imp A \imp B) \imp B \imp A \imp C
13 9, 12 mp 
(A \imp B \imp (A \imp B) \imp A \imp C) \imp (A \imp B \imp A \imp B) \imp A \imp B \imp A \imp C
14 8, 13 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp B) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  A \imp
  C
15 imp_for_imp_left_intro 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C) \imp
  (((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  (A \imp B) \imp
  A \imp
  C
16 imp_for_imp_right_left_intro 
(((A \imp B) \imp A \imp C) \imp B \imp (A \imp B) \imp A \imp C) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C
17 imp_for_imp_right_left_intro 
(((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C) \imp ((A \imp B) \imp A \imp C) \imp B \imp (A \imp B) \imp A \imp C
18 imp_reflect 
((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C
19 17, 18 mp 
((A \imp B) \imp A \imp C) \imp B \imp (A \imp B) \imp A \imp C
20 16, 19 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C
21 15, 20 mp 
(((A \imp B) \imp A \imp C) \imp (A \imp B) \imp A \imp C) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C
22 21, 18 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp (A \imp B) \imp A \imp C
23 14, 22 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp B) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp C
24 mp_imp_left_intro 
((A \imp B \imp B \imp A \imp B) \imp (A \imp B \imp B) \imp A \imp B \imp A \imp B) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp B \imp A \imp B) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp B) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  A \imp
  B
25 mp_imp_left_intro 
((B \imp B \imp A \imp B) \imp (B \imp B) \imp B \imp A \imp B) \imp (A \imp B \imp B \imp A \imp B) \imp (A \imp B \imp B) \imp A \imp B \imp A \imp B
26 mp_imp_left_intro 
((B \imp A \imp B) \imp B \imp A \imp B) \imp (B \imp B \imp A \imp B) \imp (B \imp B) \imp B \imp A \imp B
27 mp_curried 
(B \imp A \imp B) \imp B \imp A \imp B
28 26, 27 mp 
(B \imp B \imp A \imp B) \imp (B \imp B) \imp B \imp A \imp B
29 25, 28 mp 
(A \imp B \imp B \imp A \imp B) \imp (A \imp B \imp B) \imp A \imp B \imp A \imp B
30 24, 29 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp B \imp A \imp B) \imp
  (((A \imp B) \imp A \imp C) \imp A \imp B \imp B) \imp
  ((A \imp B) \imp A \imp C) \imp
  A \imp
  B \imp
  A \imp
  B
31 imp_left_intro 
(A \imp B \imp B \imp A \imp B) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp B \imp A \imp B
32 imp_left_intro 
(B \imp B \imp A \imp B) \imp A \imp B \imp B \imp A \imp B
33 imp_left_intro 
(B \imp A \imp B) \imp B \imp B \imp A \imp B
34 imp_left_intro 
B \imp A \imp B
35 33, 34 mp 
B \imp B \imp A \imp B
36 32, 35 mp 
A \imp B \imp B \imp A \imp B
37 31, 36 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp B \imp A \imp B
38 30, 37 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp B) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp B
39 imp_left_intro 
(A \imp B \imp B) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp B
40 imp_left_intro 
(B \imp B) \imp A \imp B \imp B
41 imp_reflect 
B \imp B
42 40, 41 mp 
A \imp B \imp B
43 39, 42 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp B
44 38, 43 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp B
45 23, 44 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp A \imp C
46 7, 45 mp 
(((A \imp B) \imp A \imp C) \imp A \imp B \imp A) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp C
47 imp_for_imp_left_intro 
((A \imp A) \imp A \imp B \imp A) \imp (((A \imp B) \imp A \imp C) \imp A \imp A) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp A
48 imp_for_imp_left_intro 
(A \imp B \imp A) \imp (A \imp A) \imp A \imp B \imp A
49 imp_for_imp_right_left_intro 
(A \imp A) \imp A \imp B \imp A
50 imp_reflect 
A \imp A
51 49, 50 mp 
A \imp B \imp A
52 48, 51 mp 
(A \imp A) \imp A \imp B \imp A
53 47, 52 mp 
(((A \imp B) \imp A \imp C) \imp A \imp A) \imp ((A \imp B) \imp A \imp C) \imp A \imp B \imp A
54 imp_left_intro 
(A \imp A) \imp ((A \imp B) \imp A \imp C) \imp A \imp A
55 54, 50 mp 
((A \imp B) \imp A \imp C) \imp A \imp A
56 53, 55 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp A
57 46, 56 mp 
((A \imp B) \imp A \imp C) \imp A \imp B \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)