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

Theorem pm2.01d 164
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 21 . 2  |-  ( -. 
ps  ->  -.  ps )
31, 2pm2.61d1 154 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.65d  169  pm2.01da  431  swopo  4515  oalimcl  6805  rankcf  8654  prlem934  8912  supsrlem  8988  rpnnen1lem5  10606  rennim  12046  smu01lem  12999  opsrtoslem2  16547  cfinufil  17962  alexsub  18078  ostth3  21334  cvnref  23796  pconcon  24920  untelirr  25159  dfon2lem4  25415  amosym1  26178  heiborlem10  26531  4cyclusnfrgra  28471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator