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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpii  47  pm2.43d  54  impt  180  bropfvvvv  8092  tfrlem9  8377  axcc2lem  10495  axdc3lem4  10512  fpwwe2lem7  10703  tskcard  10847  nqereu  10995  lbzbi  13044  fleqceilz  13974  ndvdsadd  16560  gcdneg  16674  ulmcaulem  26703  wlkiswwlks1  30438  elwspths2on  30533  elwspths2onw  30534  relowlpssretop  38255  poimirlem18  38524  heicant  38541  brabg2  38619  neificl  38655  eldisjdmqsim  39717  el1fzopredsuc  48340  isubgr3stgrlem3  49010