Theorem pm2.01d 174

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 164	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  180  pm2.01da  449  swopo  4770  oalimcl  7279  rankcf  9220  prlem934  9476  supsrlem  9553  rpnnen1lem5  11317  rennim  13379  smu01lem  14538  opsrtoslem2  18785  cfinufil  21021  alexsub  21138  ostth3  24555  4cyclusnfrgra  25826  cvnref  28025  pconcon  30026  untelirr  30407  dfon2lem4  30503  heiborlem10  32216  lindslinindsimp1  40758