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  171  sbcimdv  3742  predpo  5998  bropfvvvv  7588  wfrlem12  7763  tfrlem9  7818  axcc2lem  9648  axdc3lem4  9665  fpwwe2lem8  9849  tskcard  9993  nqereu  10141  lbzbi  12143  fleqceilz  13030  ndvdsadd  15611  gcdneg  15720  ulmcaulem  24675  wlkiswwlks1  27343  elwspths2on  27456  relowlpssretop  34022  poimirlem18  34299  heicant  34316  brabg2  34381  neificl  34418  el1fzopredsuc  42877