Theorem imp_left_merge_neg_imp ≪ | index | src | ≫

→左合并¬→

theorem imp_left_merge_neg_imp (A B C: wff):
  $ (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C $;
StepHypRefExpression
1 imp_for_imp_left_permute 
((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_for_imp_right_reverse_intro 
((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 neg_in_imp_reverse_intro 
(B \imp C) \imp \neg C \imp \neg B
4 2, 3 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_for_imp_left_permute 
((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_for_imp_right_reverse_intro 
((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 neg_in_imp_reverse_intro 
(A \imp C) \imp \neg C \imp \neg A
8 6, 7 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_trans_curried 
((\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_for_imp_right_reverse_intro 
((\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_for_imp_left_insert 
(\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 imp_left_intro 
(\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_for_imp_right_reverse_intro 
(\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_for_imp_left_permute 
((\neg A \imp B) \imp \neg A \imp B) \imp \neg A \imp (\neg A \imp B) \imp B
15 imp_reflect 
(\neg A \imp B) \imp \neg A \imp B
16 14, 15 mp 
\neg A \imp (\neg A \imp B) \imp B
17 13, 16 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 neg_in_imp_reverse_intro 
((\neg A \imp B) \imp B) \imp \neg B \imp \neg (\neg A \imp B)
19 17, 18 mp 
\neg A \imp \neg B \imp \neg (\neg A \imp B)
20 12, 19 mp 
\neg C \imp \neg A \imp \neg B \imp \neg (\neg A \imp B)
21 11, 20 mp 
(\neg C \imp \neg A) \imp \neg C \imp \neg B \imp \neg (\neg A \imp B)
22 10, 21 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_for_imp_left_insert 
(\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 mp 
(\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp \neg C \imp \neg (\neg A \imp B)
25 9, 24 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_for_imp_left_insert 
((\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 imp_left_intro 
((\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_in_imp_reverse_elim 
(\neg C \imp \neg (\neg A \imp B)) \imp (\neg A \imp B) \imp C
29 27, 28 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 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 mp 
(\neg C \imp \neg A) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
32 8, 31 mp 
(A \imp C) \imp (\neg C \imp \neg B) \imp (\neg A \imp B) \imp C
33 5, 32 mp 
(\neg C \imp \neg B) \imp (A \imp C) \imp (\neg A \imp B) \imp C
34 4, 33 mp 
(B \imp C) \imp (A \imp C) \imp (\neg A \imp B) \imp C
35 1, 34 mp 
(A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)