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  3748  0nelop  4688  canth  6157  sdom0  7552  canthwdom  7904  cardprclem  8259  ominf4  8591  canthp1lem2  8930  pwfseqlem4  8939  pwxpndom2  8942  lbioo  11441  ubioo  11442  fzp1disj  11631  fzonel  11681  fzouzdisj  11701  hashbclem  12322  harmonic  13438  eirrlem  13603  ruclem13  13641  prmreclem6  14099  4sqlem17  14139  vdwlem12  14170  vdwnnlem3  14175  mreexmrid  14699  psgnunilem3  16120  efgredlemb  16363  efgredlem  16364  00lss  17145  alexsublem  19747  ptcmplem4  19758  nmoleub2lem3  20801  dvferm1lem  21588  dvferm2lem  21590  plyeq0lem  21810  logno1  22213  lgsval2lem  22777  pntpbnd2  22968  ubico  26209  bnj1523  32379
  Copyright terms: Public domain W3C validator