Theorem mpdi 46

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 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpii  47  pm2.43d  54  impt  180  bropfvvvv  8103  tfrlem9  8393  axcc2lem  10514  axdc3lem4  10531  fpwwe2lem7  10722  tskcard  10866  nqereu  11014  lbzbi  13063  fleqceilz  13994  ndvdsadd  16580  gcdneg  16694  ulmcaulem  26721  wlkiswwlks1  30456  elwspths2on  30551  elwspths2onw  30552  relowlpssretop  38287  poimirlem18  38556  heicant  38573  brabg2  38651  neificl  38687  eldisjdmqsim  39749  el1fzopredsuc  48395  isubgr3stgrlem3  49065