Theorem imp_mergel_neg_imp ≪ | index | src | ≫

\imp左合并\neg\imp

theorem imp_mergel_neg_imp (A B C: wff):
  $ (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C $;
StepHypRefExpression
1 imp_imp_swapl 
((B \imp C) \imp (A \imp C) \imp (\neg A \imp B) \imp C) \imp (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C
2 imp_introrevr_imp 
((B \imp C) \imp \neg C \imp \neg B) \imp
  ((\neg C \imp \neg B) \imp (A \imp C) \imp (\neg A \imp B) \imp C) \imp
  (B \imp C) \imp
  (A \imp C) \imp
  (\neg A \imp B) \imp
  C
3 imp_introrev_neg 
(B \imp C) \imp \neg C \imp \neg B
4 2, 3 ax_mp 
((\neg C \imp \neg B) \imp (A \imp C) \imp (\neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp C) \imp (\neg A \imp B) \imp C
5 imp_imp_swapl 
((A \imp C) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C) \imp (\neg C \imp \neg B) \imp (A \imp C) \imp (\neg A \imp B) \imp C
6 imp_introrevr_imp 
((A \imp C) \imp \neg C \imp \neg A) \imp
  ((\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C) \imp
  (A \imp C) \imp
  (\neg C \imp \neg B) \imp
  (\neg A \imp B) \imp
  C
7 imp_introrev_neg 
(A \imp C) \imp \neg C \imp \neg A
8 6, 7 ax_mp 
((\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C) \imp (A \imp C) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
9 imp_tran 
((\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp
  (((\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C) \imp
  (\neg C \imp \neg A) \imp
  (\neg C \imp \neg B) \imp
  (\neg A \imp B) \imp
  C
10 imp_introrevr_imp 
((\neg C \imp \neg A) \imp \neg C \imp \neg B \imp \neg (\neg A \imp B)) \imp
  ((\neg C \imp \neg B \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp
  (\neg C \imp \neg A) \imp
  (\neg C \imp \neg B) \imp
  \neg C \imp
  \neg (\neg A \imp B)
11 imp_imp_insl 
(\neg C \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg A) \imp \neg C \imp \neg B \imp \neg (\neg A \imp B)
12 introl_imp 
(\neg A \imp \neg B \imp \neg (\neg A \imp B)) \imp \neg C \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)
13 imp_introrevr_imp 
(\neg A \imp (\neg A \imp B) \imp B) \imp (((\neg A \imp B) \imp B) \imp \neg B \imp \neg (\neg A \imp B)) \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)
14 imp_imp_swapl 
((\neg A \imp B) \imp \neg A \imp B) \imp \neg A \imp (\neg A \imp B) \imp B
15 imp_refl 
(\neg A \imp B) \imp \neg A \imp B
16 14, 15 ax_mp 
\neg A \imp (\neg A \imp B) \imp B
17 13, 16 ax_mp 
(((\neg A \imp B) \imp B) \imp \neg B \imp \neg (\neg A \imp B)) \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)
18 imp_introrev_neg 
((\neg A \imp B) \imp B) \imp \neg B \imp \neg (\neg A \imp B)
19 17, 18 ax_mp 
\neg A \imp \neg B \imp \neg (\neg A \imp B)
20 12, 19 ax_mp 
\neg C \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)
21 11, 20 ax_mp 
(\neg C \imp \neg A) \imp \neg C \imp \neg B \imp \neg (\neg A \imp B)
22 10, 21 ax_mp 
((\neg C \imp \neg B \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp
  (\neg C \imp \neg A) \imp
  (\neg C \imp \neg B) \imp
  \neg C \imp
  \neg (\neg A \imp B)
23 imp_imp_insl 
(\neg C \imp \neg B \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)
24 22, 23 ax_mp 
(\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)
25 9, 24 ax_mp 
(((\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C) \imp
  (\neg C \imp \neg A) \imp
  (\neg C \imp \neg B) \imp
  (\neg A \imp B) \imp
  C
26 imp_imp_insl 
((\neg C \imp \neg B) \imp (\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C) \imp
  ((\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp
  (\neg C \imp \neg B) \imp
  (\neg A \imp B) \imp
  C
27 introl_imp 
((\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C) \imp (\neg C \imp \neg B) \imp (\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C
28 neg_imp_elimrev 
(\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C
29 27, 28 ax_mp 
(\neg C \imp \neg B) \imp (\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C
30 26, 29 ax_mp 
((\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
31 25, 30 ax_mp 
(\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
32 8, 31 ax_mp 
(A \imp C) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
33 5, 32 ax_mp 
(\neg C \imp \neg B) \imp (A \imp C) \imp (\neg A \imp B) \imp C
34 4, 33 ax_mp 
(B \imp C) \imp (A \imp C) \imp (\neg A \imp B) \imp C
35 1, 34 ax_mp 
(A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)