Theorem imp_nested_assemb_and ≪ | index | src | ≫

嵌套前件聚合\and

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)