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  8028  tfrlem9  8310  axcc2lem  10334  axdc3lem4  10351  fpwwe2lem7  10535  tskcard  10679  nqereu  10827  lbzbi  12836  fleqceilz  13760  ndvdsadd  16323  gcdneg  16435  ulmcaulem  26331  wlkiswwlks1  29847  elwspths2on  29942  elwspths2onw  29943  relowlpssretop  37429  poimirlem18  37699  heicant  37716  brabg2  37778  neificl  37814  el1fzopredsuc  47450  isubgr3stgrlem3  48093