Theorem mp_imp_left_intro ≪ | index | src | ≫

MP规则假设引入

theorem mp_imp_left_intro (A B C D: wff):
  $ (A \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C $;
StepHypRefExpression
1 imp_trans_curried 
((A \imp B \imp C) \imp (D \imp A) \imp D \imp B \imp C) \imp
  (((D \imp A) \imp D \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C) \imp
  (A \imp B \imp C) \imp
  (D \imp A) \imp
  (D \imp B) \imp
  D \imp
  C
2 imp_for_imp_left_intro 
(A \imp B \imp C) \imp (D \imp A) \imp D \imp B \imp C
3 1, 2 mp 
(((D \imp A) \imp D \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C) \imp (A \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C
4 imp_for_imp_left_intro 
((D \imp B \imp C) \imp (D \imp B) \imp D \imp C) \imp ((D \imp A) \imp D \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C
5 imp_for_imp_left_insert 
(D \imp B \imp C) \imp (D \imp B) \imp D \imp C
6 4, 5 mp 
((D \imp A) \imp D \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C
7 3, 6 mp 
(A \imp B \imp C) \imp (D \imp A) \imp (D \imp B) \imp D \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)