Theorem neg_imp_with_imp_mergel_imp ≪ | index | src | ≫

\neg\imp与\imp左合并\imp

theorem neg_imp_with_imp_mergel_imp (A B C: wff):
  $ (\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C $;
StepHypRefExpression
1 imp_tran 
((((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C) \imp ((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp B) \imp C) \imp
  ((((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp B) \imp C) \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
    C) \imp
  (((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C) \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
  C
2 imp_introl_imp 
(((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C) \imp ((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp B) \imp C
3 1, 2 ax_mp 
((((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp B) \imp C) \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
    C) \imp
  (((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C) \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
  C
4 imp_introl_imp 
(((B \imp C) \imp (\neg \neg A \imp B) \imp C) \imp (B \imp C) \imp (A \imp B) \imp C) \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
  C
5 3, 4 ax_mp 
(((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C) \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
  C
6 imp_introrevr_imp 
((A \imp B) \imp \neg \neg A \imp B) \imp ((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C
7 imp_introrevr_imp 
(\neg \neg A \imp A) \imp (A \imp B) \imp \neg \neg A \imp B
8 negneg_elim 
\neg \neg A \imp A
9 7, 8 ax_mp 
(A \imp B) \imp \neg \neg A \imp B
10 6, 9 ax_mp 
((\neg \neg A \imp B) \imp C) \imp (A \imp B) \imp C
11 5, 10 ax_mp 
((\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 C
12 imp_mergel_neg_imp 
(\neg A \imp C) \imp (B \imp C) \imp (\neg \neg A \imp B) \imp C
13 11, 12 ax_mp 
(\neg A \imp C) \imp (B \imp C) \imp (A \imp B) \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)