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  179  bropfvvvv  8038  tfrlem9  8321  axcc2lem  10356  axdc3lem4  10373  fpwwe2lem7  10558  tskcard  10702  nqereu  10850  lbzbi  12884  fleqceilz  13811  ndvdsadd  16377  gcdneg  16489  ulmcaulem  26384  wlkiswwlks1  29960  elwspths2on  30055  elwspths2onw  30056  relowlpssretop  37733  poimirlem18  38012  heicant  38029  brabg2  38091  neificl  38127  eldisjdmqsim  39191  el1fzopredsuc  47796  isubgr3stgrlem3  48466