Theorem mpdi 45

Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)

Hypotheses

Ref	Expression
mpdi.1	⊢ (𝜓 → 𝜒)
mpdi.2	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
mpdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpdi

Step	Hyp	Ref	Expression
1		mpdi.1	. . 3 ⊢ (𝜓 → 𝜒)
2	1	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpdi.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 43	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpii  46  pm2.43d  53  impt  178  sbcimdvOLD  3791  bropfvvvv  7932  wfrlem12OLD  8151  tfrlem9  8216  axcc2lem  10192  axdc3lem4  10209  fpwwe2lem7  10393  tskcard  10537  nqereu  10685  lbzbi  12676  fleqceilz  13574  ndvdsadd  16119  gcdneg  16229  ulmcaulem  25553  wlkiswwlks1  28232  elwspths2on  28325  relowlpssretop  35535  poimirlem18  35795  heicant  35812  brabg2  35874  neificl  35911  el1fzopredsuc  44817