Theorem imp_and_splitrsr ≪ | index | src | ≫

\imp\and右侧左拆分

theorem imp_and_splitrsr (A B C: wff): $ (A \imp B \and C) \imp A \imp C $;
StepHypRefExpression
1 imp_tran 
((A \imp B \and C) \imp (A \imp B) \and (A \imp C)) \imp ((A \imp B) \and (A \imp C) \imp A \imp C) \imp (A \imp B \and C) \imp A \imp C
2 imp_and_insl 
(A \imp B \and C) \imp (A \imp B) \and (A \imp C)
3 1, 2 ax_mp 
((A \imp B) \and (A \imp C) \imp A \imp C) \imp (A \imp B \and C) \imp A \imp C
4 and_splitr 
(A \imp B) \and (A \imp C) \imp A \imp C
5 3, 4 ax_mp 
(A \imp B \and C) \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)