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  178  bropfvvvv  8034  tfrlem9  8316  axcc2lem  10346  axdc3lem4  10363  fpwwe2lem7  10548  tskcard  10692  nqereu  10840  lbzbi  12849  fleqceilz  13774  ndvdsadd  16337  gcdneg  16449  ulmcaulem  26359  wlkiswwlks1  29940  elwspths2on  30035  elwspths2onw  30036  relowlpssretop  37565  poimirlem18  37835  heicant  37852  brabg2  37914  neificl  37950  el1fzopredsuc  47567  isubgr3stgrlem3  48210