Theorem mpdi 46

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 44	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  47  pm2.43d  54  impt  180  bropfvvvv  8088  tfrlem9  8373  axcc2lem  10421  axdc3lem4  10438  fpwwe2lem7  10623  tskcard  10767  nqereu  10915  lbzbi  12961  fleqceilz  13889  ndvdsadd  16469  gcdneg  16581  ulmcaulem  26535  wlkiswwlks1  30194  elwspths2on  30289  elwspths2onw  30290  relowlpssretop  37988  poimirlem18  38267  heicant  38284  brabg2  38346  neificl  38382  eldisjdmqsim  39444  el1fzopredsuc  48040  isubgr3stgrlem3  48710