Theorem and_imp_break_nested ≪ | index | src | ≫

前件\and拆解嵌套\imp

theorem and_imp_break_nested (A B C: wff):
  $ (A \and B \imp C) \imp A \imp B \imp C $;
StepHypRefExpression
1 imp_tran 
((\neg (A \imp \neg B) \imp C) \imp A \imp \neg C \imp \neg B) \imp
  ((A \imp \neg C \imp \neg B) \imp A \imp B \imp C) \imp
  (\neg (A \imp \neg B) \imp C) \imp
  A \imp
  B \imp
  C
2 imp_tran 
((\neg (A \imp \neg B) \imp C) \imp \neg C \imp A \imp \neg B) \imp
  ((\neg C \imp A \imp \neg B) \imp A \imp \neg C \imp \neg B) \imp
  (\neg (A \imp \neg B) \imp C) \imp
  A \imp
  \neg C \imp
  \neg B
3 neg_imp_swap 
(\neg (A \imp \neg B) \imp C) \imp \neg C \imp A \imp \neg B
4 2, 3 ax_mp 
((\neg C \imp A \imp \neg B) \imp A \imp \neg C \imp \neg B) \imp (\neg (A \imp \neg B) \imp C) \imp A \imp \neg C \imp \neg B
5 imp_imp_swapl 
(\neg C \imp A \imp \neg B) \imp A \imp \neg C \imp \neg B
6 4, 5 ax_mp 
(\neg (A \imp \neg B) \imp C) \imp A \imp \neg C \imp \neg B
7 1, 6 ax_mp 
((A \imp \neg C \imp \neg B) \imp A \imp B \imp C) \imp (\neg (A \imp \neg B) \imp C) \imp A \imp B \imp C
8 imp_introl_imp 
((\neg C \imp \neg B) \imp B \imp C) \imp (A \imp \neg C \imp \neg B) \imp A \imp B \imp C
9 neg_imp_elimrev 
(\neg C \imp \neg B) \imp B \imp C
10 8, 9 ax_mp 
(A \imp \neg C \imp \neg B) \imp A \imp B \imp C
11 7, 10 ax_mp 
(\neg (A \imp \neg B) \imp C) \imp A \imp B \imp C
12 11 conv and 
(A \and B \imp C) \imp A \imp B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)