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  3755  0nelop  4698  canth  6180  sdom0  7577  canthwdom  7931  cardprclem  8286  ominf4  8618  canthp1lem2  8957  pwfseqlem4  8966  pwxpndom2  8969  lbioo  11470  ubioo  11471  fzp1disj  11660  fzonel  11710  fzouzdisj  11730  hashbclem  12363  harmonic  13479  eirrlem  13644  ruclem13  13682  prmreclem6  14140  4sqlem17  14180  vdwlem12  14211  vdwnnlem3  14216  mreexmrid  14740  psgnunilem3  16161  efgredlemb  16404  efgredlem  16405  00lss  17199  alexsublem  20015  ptcmplem4  20026  nmoleub2lem3  21069  dvferm1lem  21856  dvferm2lem  21858  plyeq0lem  22078  logno1  22481  lgsval2lem  23045  pntpbnd2  23236  ubico  26526  lbioc  30346  fouriersw  30761  bnj1523  32905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator