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  8093  tfrlem9  8378  axcc2lem  10442  axdc3lem4  10459  fpwwe2lem7  10650  tskcard  10794  nqereu  10942  lbzbi  12989  fleqceilz  13919  ndvdsadd  16506  gcdneg  16618  ulmcaulem  26637  wlkiswwlks1  30343  elwspths2on  30438  elwspths2onw  30439  relowlpssretop  38126  poimirlem18  38395  heicant  38412  brabg2  38475  neificl  38511  eldisjdmqsim  39573  el1fzopredsuc  48222  isubgr3stgrlem3  48892