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  bropfvvvv  8096  wfrlem12OLD  8339  tfrlem9  8404  axcc2lem  10455  axdc3lem4  10472  fpwwe2lem7  10656  tskcard  10800  nqereu  10948  lbzbi  12957  fleqceilz  13876  ndvdsadd  16434  gcdneg  16546  ulmcaulem  26360  wlkiswwlks1  29854  elwspths2on  29947  relowlpssretop  37387  poimirlem18  37667  heicant  37684  brabg2  37746  neificl  37782  el1fzopredsuc  47334  isubgr3stgrlem3  47960