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  3636  0nelop  4576  canth  6044  sdom0  7435  canthwdom  7786  cardprclem  8141  ominf4  8473  canthp1lem2  8812  pwfseqlem4  8821  pwxpndom2  8824  lbioo  11323  ubioo  11324  fzp1disj  11507  fzonel  11557  fzouzdisj  11577  hashbclem  12197  harmonic  13313  eirrlem  13478  ruclem13  13516  prmreclem6  13974  4sqlem17  14014  vdwlem12  14045  vdwnnlem3  14050  mreexmrid  14573  psgnunilem3  15993  efgredlemb  16234  efgredlem  16235  00lss  17000  alexsublem  19591  ptcmplem4  19602  nmoleub2lem3  20645  dvferm1lem  21431  dvferm2lem  21433  plyeq0lem  21653  logno1  22056  lgsval2lem  22620  pntpbnd2  22811  ubico  26016  bnj1523  31949
  Copyright terms: Public domain W3C validator