MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.01d Structured version   Visualization version   Unicode version

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
StepHypRef Expression
1 pm2.01d.1 . 2  |-  ( ph  ->  ( ps  ->  -.  ps ) )
2 id 22 . 2  |-  ( -. 
ps  ->  -.  ps )
31, 2pm2.61d1 164 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator