Theorem pm2.01d 181

Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem pm2.01d

Step	Hyp	Ref	Expression
1		pm2.01d.1	. 2 |- ( ph -> ( ps -> -. ps ) )
2		id 22	. 2 |- ( -. ps -> -. ps )
3	1, 2	pm2.61d1 171	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:  pm2.65d  187  pm2.01da  458  swopo  5045  onssneli  5837  oalimcl  7640  rankcf  9599  prlem934  9855  supsrlem  9932  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  rennim  13979  smu01lem  15207  opsrtoslem2  19485  cfinufil  21732  alexsub  21849  ostth3  25327  4cyclusnfrgr  27156  cvnref  29150  pconnconn  31213  untelirr  31585  dfon2lem4  31691  heiborlem10  33619  lindslinindsimp1  42246