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  4324  efrirr  4374  oalimcl  6558  omlimcl  6576  hartogslem1  7257  cfslb2n  7894  fin23lem41  7978  rankcf  8399  tskuni  8405  prlem934  8657  supsrlem  8733  rpnnen1lem5  10346  rennim  11724  smu01lem  12676  4sqlem18  13009  opsrtoslem2  16226  cfinufil  17623  alexsub  17739  ivthlem2  18812  ivthlem3  18813  cosne0  19892  ostth3  20787  cvnref  22871  pconcon  23762  untelirr  24054  dfon2lem4  24142  amosym1  24865  lppotoslem  26143  heiborlem10  26544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator