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  8096  tfrlem9  8381  axcc2lem  10438  axdc3lem4  10455  fpwwe2lem7  10640  tskcard  10784  nqereu  10932  lbzbi  12978  fleqceilz  13907  ndvdsadd  16493  gcdneg  16605  ulmcaulem  26594  wlkiswwlks1  30253  elwspths2on  30348  elwspths2onw  30349  relowlpssretop  38051  poimirlem18  38330  heicant  38347  brabg2  38409  neificl  38445  eldisjdmqsim  39507  el1fzopredsuc  48104  isubgr3stgrlem3  48774