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  sbcimdvOLD  3787  bropfvvvv  7903  wfrlem12OLD  8122  tfrlem9  8187  axcc2lem  10123  axdc3lem4  10140  fpwwe2lem7  10324  tskcard  10468  nqereu  10616  lbzbi  12605  fleqceilz  13502  ndvdsadd  16047  gcdneg  16157  ulmcaulem  25458  wlkiswwlks1  28133  elwspths2on  28226  relowlpssretop  35462  poimirlem18  35722  heicant  35739  brabg2  35801  neificl  35838  el1fzopredsuc  44705