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

Theorem pm2.65i 173
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 120 . 2
3 pm2.65i.1 . . 3
43con3i 135 . 2
52, 4pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.21dd  174  mto  176  mt2  179  noel  3788  0nelop  4742  canth  6254  sdom0  7669  canthwdom  8026  cardprclem  8381  ominf4  8713  canthp1lem2  9052  pwfseqlem4  9061  pwxpndom2  9064  lbioo  11589  ubioo  11590  fzp1disj  11767  fzonel  11841  fzouzdisj  11861  hashbclem  12501  harmonic  13670  eirrlem  13937  ruclem13  13975  prmreclem6  14439  4sqlem17  14479  vdwlem12  14510  vdwnnlem3  14515  mreexmrid  15040  psgnunilem3  16521  efgredlemb  16764  efgredlem  16765  00lss  17588  alexsublem  20544  ptcmplem4  20555  nmoleub2lem3  21598  dvferm1lem  22385  dvferm2lem  22387  plyeq0lem  22607  logno1  23017  lgsval2lem  23581  pntpbnd2  23772  ubico  27586  pm2.65ni  31439  lbioc  31553  bnj1523  34127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator