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  181  sbcimdvOLD  3757  predpo  6158  bropfvvvv  7838  wfrlem12  8044  tfrlem9  8099  axcc2lem  10015  axdc3lem4  10032  fpwwe2lem7  10216  tskcard  10360  nqereu  10508  lbzbi  12497  fleqceilz  13392  ndvdsadd  15934  gcdneg  16044  ulmcaulem  25240  wlkiswwlks1  27905  elwspths2on  27998  relowlpssretop  35221  poimirlem18  35481  heicant  35498  brabg2  35560  neificl  35597  el1fzopredsuc  44433