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

Theorem pm2.01d 172
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 162 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  178  pm2.01da  443  swopo  4727  oalimcl  7216  rankcf  9153  prlem934  9409  supsrlem  9486  rpnnen1lem5  11245  rennim  13246  smu01lem  14402  opsrtoslem2  18651  cfinufil  20885  alexsub  21002  ostth3  24418  4cyclusnfrgra  25689  cvnref  27886  pconcon  29906  untelirr  30287  dfon2lem4  30383  amosym1  31035  heiborlem10  32059  lindslinindsimp1  39843
  Copyright terms: Public domain W3C validator