Theorem imp_and_insl ≪ | index | src | ≫

\imp\and左插入

theorem imp_and_insl (A B C: wff):
  $ (A \imp B \and C) \imp (A \imp B) \and (A \imp C) $;
StepHypRefExpression
1 imp_collectr_and 
((A \imp B \and C) \imp A \imp B) \imp ((A \imp B \and C) \imp A \imp C) \imp (A \imp B \and C) \imp (A \imp B) \and (A \imp C)
2 imp_tran 
((B \and C \imp B) \imp (A \imp B \and C) \imp A \imp B) \imp
  (((A \imp B \and C) \imp A \imp B) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp B) \imp
  (B \and C \imp B) \imp
  ((A \imp B \and C) \imp A \imp B \and C) \imp
  (A \imp B \and C) \imp
  A \imp
  B
3 imp_introl_imp 
(B \and C \imp B) \imp (A \imp B \and C) \imp A \imp B
4 2, 3 ax_mp 
(((A \imp B \and C) \imp A \imp B) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp B) \imp
  (B \and C \imp B) \imp
  ((A \imp B \and C) \imp A \imp B \and C) \imp
  (A \imp B \and C) \imp
  A \imp
  B
5 imp_introl_imp 
((A \imp B \and C) \imp A \imp B) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp B
6 4, 5 ax_mp 
(B \and C \imp B) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp B
7 and_splitl 
B \and C \imp B
8 6, 7 ax_mp 
((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp B
9 imp_refl 
(A \imp B \and C) \imp A \imp B \and C
10 8, 9 ax_mp 
(A \imp B \and C) \imp A \imp B
11 1, 10 ax_mp 
((A \imp B \and C) \imp A \imp C) \imp (A \imp B \and C) \imp (A \imp B) \and (A \imp C)
12 imp_tran 
((B \and C \imp C) \imp (A \imp B \and C) \imp A \imp C) \imp
  (((A \imp B \and C) \imp A \imp C) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp C) \imp
  (B \and C \imp C) \imp
  ((A \imp B \and C) \imp A \imp B \and C) \imp
  (A \imp B \and C) \imp
  A \imp
  C
13 imp_introl_imp 
(B \and C \imp C) \imp (A \imp B \and C) \imp A \imp C
14 12, 13 ax_mp 
(((A \imp B \and C) \imp A \imp C) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp C) \imp
  (B \and C \imp C) \imp
  ((A \imp B \and C) \imp A \imp B \and C) \imp
  (A \imp B \and C) \imp
  A \imp
  C
15 imp_introl_imp 
((A \imp B \and C) \imp A \imp C) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp C
16 14, 15 ax_mp 
(B \and C \imp C) \imp ((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp C
17 and_splitr 
B \and C \imp C
18 16, 17 ax_mp 
((A \imp B \and C) \imp A \imp B \and C) \imp (A \imp B \and C) \imp A \imp C
19 18, 9 ax_mp 
(A \imp B \and C) \imp A \imp C
20 11, 19 ax_mp 
(A \imp B \and C) \imp (A \imp B) \and (A \imp C)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)