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  8103  tfrlem9  8396  axcc2lem  10517  axdc3lem4  10534  fpwwe2lem7  10725  tskcard  10869  nqereu  11017  lbzbi  13066  fleqceilz  13997  ndvdsadd  16585  gcdneg  16699  ulmcaulem  26726  wlkiswwlks1  30461  elwspths2on  30556  elwspths2onw  30557  relowlpssretop  38380  poimirlem18  38649  heicant  38666  brabg2  38744  neificl  38780  eldisjdmqsim  39842  el1fzopredsuc  48489  isubgr3stgrlem3  49159