Theorem mpdi 44

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 42	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  45  pm2.43d  51  impt  168  sbcimdv  3465  predpo  5615  suctrOLD  5726  bropfvvvv  7144  wfrlem12  7313  tfrlem9  7368  axcc2lem  9141  axdc3lem4  9158  fpwwe2lem8  9338  tskcard  9482  nqereu  9630  lbzbi  11652  fleqceilz  12515  ndvdsadd  14972  gcdneg  15081  ulmcaulem  23952  wlkiswwlk1  26218  frgrawopreglem4  26574  frrlem11  31036  relowlpssretop  32388  poimirlem18  32597  heicant  32614  brabg2  32680  neificl  32719  el1fzopredsuc  39948  frgrwopreglem4  41484