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  8044  tfrlem9  8326  axcc2lem  10358  axdc3lem4  10375  fpwwe2lem7  10560  tskcard  10704  nqereu  10852  lbzbi  12861  fleqceilz  13786  ndvdsadd  16349  gcdneg  16461  ulmcaulem  26371  wlkiswwlks1  29952  elwspths2on  30047  elwspths2onw  30048  relowlpssretop  37613  poimirlem18  37883  heicant  37900  brabg2  37962  neificl  37998  eldisjdmqsim  39062  el1fzopredsuc  47679  isubgr3stgrlem3  48322