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  179  bropfvvvv  8066  tfrlem9  8351  axcc2lem  10390  axdc3lem4  10407  fpwwe2lem7  10592  tskcard  10736  nqereu  10884  lbzbi  12934  fleqceilz  13861  ndvdsadd  16427  gcdneg  16539  ulmcaulem  26434  wlkiswwlks1  30013  elwspths2on  30108  elwspths2onw  30109  relowlpssretop  37822  poimirlem18  38101  heicant  38118  brabg2  38180  neificl  38216  eldisjdmqsim  39280  el1fzopredsuc  47884  isubgr3stgrlem3  48554