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  8046  tfrlem9  8328  axcc2lem  10360  axdc3lem4  10377  fpwwe2lem7  10562  tskcard  10706  nqereu  10854  lbzbi  12863  fleqceilz  13788  ndvdsadd  16351  gcdneg  16463  ulmcaulem  26376  wlkiswwlks1  29958  elwspths2on  30053  elwspths2onw  30054  relowlpssretop  37646  poimirlem18  37918  heicant  37935  brabg2  37997  neificl  38033  eldisjdmqsim  39097  el1fzopredsuc  47714  isubgr3stgrlem3  48357