Theorem pm2.18d 115

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 114	. 2 |- ( ( -. ps -> ps ) -> ps )
3	1, 2	syl 17	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  notnot2  116  pm2.61d  162  pm2.18da  445  oplem1  975  axc11n  2143  axc11nALT  2144  weniso  6245  infssuni  7865  ordtypelem10  8042  oismo  8055  rankval3b  8297  grur1  9245  sqeqd  13229  hausflimi  20995  minveclem4  22374  minveclem4OLD  22386  ovolunnul  22453  vitali  22571  itg2mono  22711  pilem3  23409  pilem3OLD  23410  frgrancvvdeqlemB  25766  minvecolem4  26522  minvecolem4OLD  26532  bj-axc11nv  31348  contrd  32333