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

Theorem pm2.65i 168
Description: Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
pm2.65i.1
pm2.65i.2
Assertion
Ref Expression
pm2.65i

Proof of Theorem pm2.65i
StepHypRef Expression
1 pm2.65i.2 . . 3
21con2i 115 . 2
3 pm2.65i.1 . . 3
43con3i 130 . 2
52, 4pm2.61i 159 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  mto  170  mt2  173  noel  3618  0nelop  4553  canth  6017  sdom0  7402  canthwdom  7741  cardprclem  8096  ominf4  8428  canthp1lem2  8766  pwfseqlem4  8775  pwxpndom2  8778  lbioo  11276  ubioo  11277  fzp1disj  11457  fzonel  11506  fzouzdisj  11526  hashbclem  12146  harmonic  13261  eirrlem  13426  ruclem13  13464  prmreclem6  13922  4sqlem17  13962  vdwlem12  13993  vdwnnlem3  13998  mreexmrid  14521  psgnunilem3  15939  efgredlemb  16180  efgredlem  16181  00lss  16832  alexsublem  19320  ptcmplem4  19331  nmoleub2lem3  20370  dvferm1lem  21156  dvferm2lem  21158  plyeq0lem  21419  logno1  21822  lgsval2lem  22386  pntpbnd2  22577  ubico  25743  bnj1523  31640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator