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  180  sbcimdv  3840  predpo  6163  bropfvvvv  7784  wfrlem12  7963  tfrlem9  8018  axcc2lem  9855  axdc3lem4  9872  fpwwe2lem8  10056  tskcard  10200  nqereu  10348  lbzbi  12334  fleqceilz  13220  ndvdsadd  15757  gcdneg  15866  ulmcaulem  24980  wlkiswwlks1  27643  elwspths2on  27737  relowlpssretop  34672  poimirlem18  34948  heicant  34965  brabg2  35027  neificl  35064  el1fzopredsuc  43599