Theorem imp_left_have_neg_merge ≪ | index | src | ≫

→左含¬合并

theorem imp_left_have_neg_merge (A B C: wff):
  $ (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C $;
StepHypRefExpression
1 mp_imp_left_intro 
(((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (B \imp C) \imp (A \imp B) \imp C)
  \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  C
2 mp_imp_left_intro 
(((A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp ((A \imp B) \imp \neg \neg A \imp B) \imp (A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  C
3 mp_imp_left_intro 
(((\neg \neg A \imp B) \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp \neg \neg A \imp B) \imp
  (A \imp B) \imp
  C
4 mp_curried 
((\neg \neg A \imp B) \imp C) \imp (\neg \neg A \imp B) \imp C
5 3, 4 mp 
((A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp ((A \imp B) \imp \neg \neg A \imp B) \imp (A \imp B) \imp C
6 2, 5 mp 
((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (B \imp C) \imp (A \imp B) \imp C
7 1, 6 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  C
8 mp_imp_left_intro 
(((B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
    ((B \imp C) \imp (A \imp B) \imp B \imp C) \imp
    (B \imp C) \imp
    (A \imp B) \imp
    (\neg \neg A \imp B) \imp
    C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp B) \imp
  C
9 mp_imp_left_intro 
(((A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp ((A \imp B) \imp B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp B \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp B) \imp
  C
10 mp_imp_left_intro 
(((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp B) \imp
  C
11 mp_curried 
((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
12 10, 11 mp 
((A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp ((A \imp B) \imp B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C
13 9, 12 mp 
((B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp B \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp B) \imp
  C
14 8, 13 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp B) \imp
  C
15 mp_imp_left_intro 
(((B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
    ((B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
    (B \imp C) \imp
    (A \imp B) \imp
    (B \imp C) \imp
    (\neg \neg A \imp B) \imp
    C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
16 mp_imp_left_intro 
(((A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
    ((A \imp B) \imp \neg A \imp C) \imp
    (A \imp B) \imp
    (B \imp C) \imp
    (\neg \neg A \imp B) \imp
    C) \imp
  ((B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
17 mp_imp_left_intro 
(((\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp \neg A \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
18 mp_curried 
((\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
19 17, 18 mp 
((A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((A \imp B) \imp \neg A \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
20 16, 19 mp 
((B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
21 15, 20 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
22 imp_left_intro 
((B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
23 imp_left_intro 
((A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
24 imp_left_intro 
((\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
25 imp_left_merge_neg_imp 
(\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
26 24, 25 mp 
(A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
27 23, 26 mp 
(B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
28 22, 27 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
29 21, 28 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (B \imp C) \imp
  (\neg \neg A \imp B) \imp
  C
30 imp_for_imp_left_intro 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp
  ((\neg A \imp C) \imp \neg A \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  \neg A \imp
  C
31 imp_for_imp_right_left_intro 
((\neg A \imp C) \imp (A \imp B) \imp \neg A \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C
32 imp_for_imp_right_left_intro 
((\neg A \imp C) \imp \neg A \imp C) \imp (\neg A \imp C) \imp (A \imp B) \imp \neg A \imp C
33 imp_reflect 
(\neg A \imp C) \imp \neg A \imp C
34 32, 33 mp 
(\neg A \imp C) \imp (A \imp B) \imp \neg A \imp C
35 31, 34 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C
36 30, 35 mp 
((\neg A \imp C) \imp \neg A \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C
37 36, 33 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg A \imp C
38 29, 37 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
39 14, 38 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C
40 imp_for_imp_left_intro 
(((B \imp C) \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp B \imp C) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  B \imp
  C
41 imp_for_imp_left_intro 
((B \imp C) \imp (A \imp B) \imp B \imp C) \imp ((B \imp C) \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C
42 imp_for_imp_right_left_intro 
((B \imp C) \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C
43 imp_reflect 
(B \imp C) \imp B \imp C
44 42, 43 mp 
(B \imp C) \imp (A \imp B) \imp B \imp C
45 41, 44 mp 
((B \imp C) \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C
46 40, 45 mp 
((\neg A \imp C) \imp (B \imp C) \imp B \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C
47 imp_left_intro 
((B \imp C) \imp B \imp C) \imp (\neg A \imp C) \imp (B \imp C) \imp B \imp C
48 47, 43 mp 
(\neg A \imp C) \imp (B \imp C) \imp B \imp C
49 46, 48 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp B \imp C
50 39, 49 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp B) \imp C
51 7, 50 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C
52 mp_imp_left_intro 
(((B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
    ((B \imp C) \imp (A \imp B) \imp A \imp B) \imp
    (B \imp C) \imp
    (A \imp B) \imp
    \neg \neg A \imp
    B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
53 mp_imp_left_intro 
(((A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp ((A \imp B) \imp A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((B \imp C) \imp (A \imp B) \imp A \imp B) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
54 mp_imp_left_intro 
(((A \imp B) \imp \neg \neg A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((A \imp B) \imp A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
55 mp_curried 
((A \imp B) \imp \neg \neg A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B
56 54, 55 mp 
((A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp ((A \imp B) \imp A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B
57 53, 56 mp 
((B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((B \imp C) \imp (A \imp B) \imp A \imp B) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
58 52, 57 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
59 mp_imp_left_intro 
(((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
    ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
    (B \imp C) \imp
    (A \imp B) \imp
    (A \imp B) \imp
    \neg \neg A \imp
    B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
60 mp_imp_left_intro 
(((A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
    ((A \imp B) \imp \neg \neg A \imp A) \imp
    (A \imp B) \imp
    (A \imp B) \imp
    \neg \neg A \imp
    B) \imp
  ((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
61 mp_imp_left_intro 
(((\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((A \imp B) \imp \neg \neg A \imp A) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
62 mp_curried 
((\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
63 61, 62 mp 
((A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((A \imp B) \imp \neg \neg A \imp A) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
64 60, 63 mp 
((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
65 59, 64 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  ((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
66 imp_left_intro 
((B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp A) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
67 imp_left_intro 
((A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (\neg \neg A \imp A) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
68 imp_left_intro 
((\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
69 imp_trans_curried 
(\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
70 68, 69 mp 
(A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
71 67, 70 mp 
(B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
72 66, 71 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
73 65, 72 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp
  (\neg A \imp C) \imp
  (B \imp C) \imp
  (A \imp B) \imp
  (A \imp B) \imp
  \neg \neg A \imp
  B
74 imp_left_intro 
((B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A
75 imp_left_intro 
((A \imp B) \imp \neg \neg A \imp A) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A
76 imp_left_intro 
(\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp A
77 neg_neg_elim 
\neg \neg A \imp A
78 76, 77 mp 
(A \imp B) \imp \neg \neg A \imp A
79 75, 78 mp 
(B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A
80 74, 79 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp A
81 73, 80 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp (A \imp B) \imp \neg \neg A \imp B
82 58, 81 mp 
((\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B
83 imp_left_intro 
((B \imp C) \imp (A \imp B) \imp A \imp B) \imp (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp B
84 imp_left_intro 
((A \imp B) \imp A \imp B) \imp (B \imp C) \imp (A \imp B) \imp A \imp B
85 imp_reflect 
(A \imp B) \imp A \imp B
86 84, 85 mp 
(B \imp C) \imp (A \imp B) \imp A \imp B
87 83, 86 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp B
88 82, 87 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp \neg \neg A \imp B
89 51, 88 mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)