Theorem mpdi 45

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpii  46  pm2.43d  53  impt  178  bropfvvvv  8100  wfrlem12OLD  8343  tfrlem9  8408  axcc2lem  10459  axdc3lem4  10476  fpwwe2lem7  10660  tskcard  10804  nqereu  10952  lbzbi  12961  fleqceilz  13877  ndvdsadd  16430  gcdneg  16542  ulmcaulem  26392  wlkiswwlks1  29834  elwspths2on  29927  relowlpssretop  37306  poimirlem18  37586  heicant  37603  brabg2  37665  neificl  37701  el1fzopredsuc  47283  isubgr3stgrlem3  47881