MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.01d 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
Assertion
Ref Expression
pm2.01d

Proof of Theorem pm2.01d
StepHypRef Expression
1 pm2.01d.1 . 2
2 id 22 . 2
31, 2pm2.61d1 159 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.65d  175  pm2.01da  442  swopo  4815  oalimcl  7228  rankcf  9176  prlem934  9432  supsrlem  9509  rpnnen1lem5  11241  rennim  13072  smu01lem  14135  opsrtoslem2  18149  cfinufil  20429  alexsub  20545  ostth3  23823  4cyclusnfrgra  25019  cvnref  27210  pconcon  28676  untelirr  29080  dfon2lem4  29218  amosym1  29891  heiborlem10  30316  lindslinindsimp1  33058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator