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

Theorem pm2.01d 169
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 159 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  175  pm2.01da  442  swopo  4760  oalimcl  7110  rankcf  9056  prlem934  9314  supsrlem  9390  rpnnen1lem5  11095  rennim  12847  smu01lem  13800  opsrtoslem2  17691  cfinufil  19634  alexsub  19750  ostth3  23021  cvnref  25848  pconcon  27265  untelirr  27504  dfon2lem4  27744  amosym1  28417  heiborlem10  28868  4cyclusnfrgra  30760  lindslinindsimp1  31124
  Copyright terms: Public domain W3C validator