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  8128  tfrlem9  8421  axcc2lem  10541  axdc3lem4  10558  fpwwe2lem7  10749  tskcard  10893  nqereu  11041  lbzbi  13090  fleqceilz  14021  ndvdsadd  16609  gcdneg  16723  ulmcaulem  26751  wlkiswwlks1  30486  elwspths2on  30581  elwspths2onw  30582  relowlpssretop  38479  poimirlem18  38748  heicant  38765  brabg2  38843  neificl  38879  eldisjdmqsim  39941  el1fzopredsuc  48601  isubgr3stgrlem3  49271