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  3866  bropfvvvv  8116  wfrlem12OLD  8359  tfrlem9  8424  axcc2lem  10474  axdc3lem4  10491  fpwwe2lem7  10675  tskcard  10819  nqereu  10967  lbzbi  12976  fleqceilz  13891  ndvdsadd  16444  gcdneg  16556  ulmcaulem  26452  wlkiswwlks1  29897  elwspths2on  29990  relowlpssretop  37347  poimirlem18  37625  heicant  37642  brabg2  37704  neificl  37740  el1fzopredsuc  47275  isubgr3stgrlem3  47871