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

Theorem pm2.01d 161
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 19 . 2  |-  ( -. 
ps  ->  -.  ps )
31, 2pm2.61d1 151 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.65d  166  pm2.01da  429  swopo  4361  efrirr  4411  oalimcl  6600  omlimcl  6618  hartogslem1  7302  cfslb2n  7939  fin23lem41  8023  rankcf  8444  tskuni  8450  prlem934  8702  supsrlem  8778  rpnnen1lem5  10393  rennim  11771  smu01lem  12723  4sqlem18  13056  opsrtoslem2  16275  cfinufil  17675  alexsub  17791  ivthlem2  18865  ivthlem3  18866  cosne0  19945  ostth3  20840  cvnref  22926  pconcon  24046  untelirr  24338  dfon2lem4  24527  amosym1  25251  heiborlem10  25692  4cyclusnfrgra  27611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator