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  8042  tfrlem9  8324  axcc2lem  10358  axdc3lem4  10375  fpwwe2lem7  10560  tskcard  10704  nqereu  10852  lbzbi  12886  fleqceilz  13813  ndvdsadd  16379  gcdneg  16491  ulmcaulem  26359  wlkiswwlks1  29935  elwspths2on  30030  elwspths2onw  30031  relowlpssretop  37680  poimirlem18  37959  heicant  37976  brabg2  38038  neificl  38074  eldisjdmqsim  39138  el1fzopredsuc  47774  isubgr3stgrlem3  48444