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  sbcimdvOLD  3879  bropfvvvv  8133  wfrlem12OLD  8376  tfrlem9  8441  axcc2lem  10505  axdc3lem4  10522  fpwwe2lem7  10706  tskcard  10850  nqereu  10998  lbzbi  13001  fleqceilz  13905  ndvdsadd  16458  gcdneg  16568  ulmcaulem  26455  wlkiswwlks1  29900  elwspths2on  29993  relowlpssretop  37330  poimirlem18  37598  heicant  37615  brabg2  37677  neificl  37713  el1fzopredsuc  47240