Theorem imp_and_extl ≪ | index | src | ≫

\imp对\and左提取

theorem imp_and_extl (A B C: wff):
  $ (A \imp B) \and (A \imp C) \imp A \imp B \and C $;
StepHypRefExpression
1 and_imp_break_nested 
((A \imp B) \and (A \imp C) \and A \imp B \and C) \imp (A \imp B) \and (A \imp C) \imp A \imp B \and C
2 mp_with_ant_thm 
((A \imp B) \and (A \imp C) \and A \imp C \imp B \and C) \imp ((A \imp B) \and (A \imp C) \and A \imp C) \imp (A \imp B) \and (A \imp C) \and A \imp B \and C
3 imp_introl_imp 
(B \imp C \imp B \and C) \imp ((A \imp B) \and (A \imp C) \and A \imp B) \imp (A \imp B) \and (A \imp C) \and A \imp C \imp B \and C
4 and_comp 
B \imp C \imp B \and C
5 3, 4 ax_mp 
((A \imp B) \and (A \imp C) \and A \imp B) \imp (A \imp B) \and (A \imp C) \and A \imp C \imp B \and C
6 imp_nested_assemb_and 
((A \imp B) \and (A \imp C) \imp A \imp B) \imp (A \imp B) \and (A \imp C) \and A \imp B
7 and_splitl 
(A \imp B) \and (A \imp C) \imp A \imp B
8 6, 7 ax_mp 
(A \imp B) \and (A \imp C) \and A \imp B
9 5, 8 ax_mp 
(A \imp B) \and (A \imp C) \and A \imp C \imp B \and C
10 2, 9 ax_mp 
((A \imp B) \and (A \imp C) \and A \imp C) \imp (A \imp B) \and (A \imp C) \and A \imp B \and C
11 imp_nested_assemb_and 
((A \imp B) \and (A \imp C) \imp A \imp C) \imp (A \imp B) \and (A \imp C) \and A \imp C
12 and_splitr 
(A \imp B) \and (A \imp C) \imp A \imp C
13 11, 12 ax_mp 
(A \imp B) \and (A \imp C) \and A \imp C
14 10, 13 ax_mp 
(A \imp B) \and (A \imp C) \and A \imp B \and C
15 1, 14 ax_mp 
(A \imp B) \and (A \imp C) \imp A \imp B \and C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)