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

Theorem pm2.65i 177
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 124 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 141 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 168 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  178  mto  180  mt2  183  noel  3766  0nelop  4708  canth  6262  sdom0  7708  canthwdom  8098  cardprclem  8416  ominf4  8744  canthp1lem2  9080  pwfseqlem4  9089  pwxpndom2  9092  lbioo  11669  ubioo  11670  fzp1disj  11856  fzonel  11935  fzouzdisj  11956  hashbclem  12614  harmonic  13910  eirrlem  14249  ruclem13  14287  prmreclem6  14858  4sqlem17OLD  14898  4sqlem17  14904  vdwlem12  14935  vdwnnlem3  14940  mreexmrid  15542  psgnunilem3  17130  efgredlemb  17389  efgredlem  17390  00lss  18158  alexsublem  21051  ptcmplem4  21062  nmoleub2lem3  22121  dvferm1lem  22928  dvferm2lem  22930  plyeq0lem  23156  logno1  23573  lgsval2lem  24226  pntpbnd2  24417  ubico  28357  bnj1523  29882  pm2.65ni  37283  lbioc  37489
  Copyright terms: Public domain W3C validator