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  8035  tfrlem9  8317  axcc2lem  10349  axdc3lem4  10366  fpwwe2lem7  10551  tskcard  10695  nqereu  10843  lbzbi  12877  fleqceilz  13804  ndvdsadd  16370  gcdneg  16482  ulmcaulem  26372  wlkiswwlks1  29950  elwspths2on  30045  elwspths2onw  30046  relowlpssretop  37694  poimirlem18  37973  heicant  37990  brabg2  38052  neificl  38088  eldisjdmqsim  39152  el1fzopredsuc  47786  isubgr3stgrlem3  48456