Theorem mpdi 59

Description: A nested modus ponens deduction. (The proof was shortened by O'Cat, 15-Jan-2008.)

Hypotheses

Ref	Expression
mpdi.1	|- (ps -> ch)
mpdi.2	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
mpdi	|- (ph -> (ps -> th))

Proof of Theorem mpdi

Step	Hyp	Ref	Expression
1		mpdi.1	. . 3 |- (ps -> ch)
2	1	a1i 8	. 2 |- (ph -> (ps -> ch))
3		mpdi.2	. 2 |- (ph -> (ps -> (ch -> th)))
4	2, 3	mpdd 57	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.43d 79  suctr 3751  fvopab2 4754  tfrlem9 5127  mulcmpblnr 6335  metcn4i 9250  gapmlem 9461  tx1cn 10223  tx2cn 10224  ismnd2 10392  fseq1cl 13619  gcdneg 13732  predso 13895  wfrlem12 13968  axfelem16 14046  inficlALT 15372  topmtcl 15525  ufilen 15579  brabg2 15681  inficl 15757  heiborlem11 15965  heiborlem16 15970  isphtpc2 16060

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain