MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65i Structured version   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  |-  ( ph  ->  ps )
pm2.65i.2  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.65i  |-  -.  ph

Proof of Theorem pm2.65i
StepHypRef Expression
1 pm2.65i.2 . . 3  |-  ( ph  ->  -.  ps )
21con2i 120 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 135 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 164 1  |-  -.  ph
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.21dd  174  mto  176  mt2  179  noel  3629  0nelop  4569  canth  6036  sdom0  7431  canthwdom  7782  cardprclem  8137  ominf4  8469  canthp1lem2  8808  pwfseqlem4  8817  pwxpndom2  8820  lbioo  11319  ubioo  11320  fzp1disj  11500  fzonel  11549  fzouzdisj  11569  hashbclem  12189  harmonic  13304  eirrlem  13469  ruclem13  13507  prmreclem6  13965  4sqlem17  14005  vdwlem12  14036  vdwnnlem3  14041  mreexmrid  14564  psgnunilem3  15982  efgredlemb  16223  efgredlem  16224  00lss  16945  alexsublem  19458  ptcmplem4  19469  nmoleub2lem3  20512  dvferm1lem  21298  dvferm2lem  21300  plyeq0lem  21563  logno1  21966  lgsval2lem  22530  pntpbnd2  22721  ubico  25888  bnj1523  31764
  Copyright terms: Public domain W3C validator