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

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  47  pm2.43d  54  impt  180  bropfvvvv  8075  tfrlem9  8360  axcc2lem  10408  axdc3lem4  10425  fpwwe2lem7  10610  tskcard  10754  nqereu  10902  lbzbi  12951  fleqceilz  13878  ndvdsadd  16458  gcdneg  16570  ulmcaulem  26515  wlkiswwlks1  30125  elwspths2on  30220  elwspths2onw  30221  relowlpssretop  37870  poimirlem18  38149  heicant  38166  brabg2  38228  neificl  38264  eldisjdmqsim  39328  el1fzopredsuc  47918  isubgr3stgrlem3  48588