Theorem pm2.18d 105

Description: Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypothesis

Ref	Expression
pm2.18d.1	|- ( ph -> ( -. ps -> ps ) )

Assertion

Ref	Expression
pm2.18d	|- ( ph -> ps )

Proof of Theorem pm2.18d

Step	Hyp	Ref	Expression
1		pm2.18d.1	. 2 |- ( ph -> ( -. ps -> ps ) )
2		pm2.18 104	. 2 |- ( ( -. ps -> ps ) -> ps )
3	1, 2	syl 16	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  notnot2  106  pm2.61d  152  pm2.18da  431  oplem1  931  ax10  1991  ax10lem4OLD  1996  weniso  6034  ordtypelem10  7452  oismo  7465  rankval3b  7708  grur1  8651  sqeqd  11926  hausflimi  17965  minveclem4  19286  ovolunnul  19349  vitali  19458  itg2mono  19598  pilem3  20322  minvecolem4  22335  frgrancvvdeqlemB  28141  ax10lem4NEW7  29177

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8