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  440  swopo  4799  oalimcl  7201  rankcf  9144  prlem934  9400  supsrlem  9477  rpnnen1lem5  11213  rennim  13154  smu01lem  14219  opsrtoslem2  18344  cfinufil  20595  alexsub  20711  ostth3  24021  4cyclusnfrgra  25221  cvnref  27408  pconcon  28940  untelirr  29321  dfon2lem4  29458  amosym1  30119  heiborlem10  30556  lindslinindsimp1  33312
  Copyright terms: Public domain W3C validator