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  3498  predpo  5698  suctrOLD  5809  bropfvvvv  7257  wfrlem12  7426  tfrlem9  7481  axcc2lem  9258  axdc3lem4  9275  fpwwe2lem8  9459  tskcard  9603  nqereu  9751  lbzbi  11776  fleqceilz  12653  ndvdsadd  15134  gcdneg  15243  ulmcaulem  24148  wlkiswwlks1  26753  frrlem11  31792  relowlpssretop  33212  poimirlem18  33427  heicant  33444  brabg2  33510  neificl  33549  el1fzopredsuc  41335