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  169  sbcimdv  3531  predpo  5736  suctrOLD  5847  bropfvvvv  7302  wfrlem12  7471  tfrlem9  7526  axcc2lem  9296  axdc3lem4  9313  fpwwe2lem8  9497  tskcard  9641  nqereu  9789  lbzbi  11814  fleqceilz  12693  ndvdsadd  15181  gcdneg  15290  ulmcaulem  24193  wlkiswwlks1  26821  elwspths2on  26926  relowlpssretop  33342  poimirlem18  33557  heicant  33574  brabg2  33640  neificl  33679  el1fzopredsuc  41660