Theorem imp_intror_and ≪ | index | src | ≫

\imp右引入\and

theorem imp_intror_and (A B C: wff): $ (A \imp B) \imp A \and C \imp B \and C $;
StepHypRefExpression
1 imp_tran 
((A \imp B) \imp (B \imp \neg C) \imp A \imp \neg C) \imp
  (((B \imp \neg C) \imp A \imp \neg C) \imp \neg (A \imp \neg C) \imp \neg (B \imp \neg C)) \imp
  (A \imp B) \imp
  \neg (A \imp \neg C) \imp
  \neg (B \imp \neg C)
2 imp_introrevr_imp 
(A \imp B) \imp (B \imp \neg C) \imp A \imp \neg C
3 1, 2 ax_mp 
(((B \imp \neg C) \imp A \imp \neg C) \imp \neg (A \imp \neg C) \imp \neg (B \imp \neg C)) \imp (A \imp B) \imp \neg (A \imp \neg C) \imp \neg (B \imp \neg C)
4 imp_introrev_neg 
((B \imp \neg C) \imp A \imp \neg C) \imp \neg (A \imp \neg C) \imp \neg (B \imp \neg C)
5 3, 4 ax_mp 
(A \imp B) \imp \neg (A \imp \neg C) \imp \neg (B \imp \neg C)
6 5 conv and 
(A \imp B) \imp A \and C \imp B \and C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)