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  3845  predpo  6168  bropfvvvv  7789  wfrlem12  7968  tfrlem9  8023  axcc2lem  9860  axdc3lem4  9877  fpwwe2lem8  10061  tskcard  10205  nqereu  10353  lbzbi  12339  fleqceilz  13225  ndvdsadd  15763  gcdneg  15872  ulmcaulem  24984  wlkiswwlks1  27647  elwspths2on  27741  relowlpssretop  34647  poimirlem18  34912  heicant  34929  brabg2  34993  neificl  35030  el1fzopredsuc  43532