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  3787  0nelop  4726  canth  6229  sdom0  7642  canthwdom  7997  cardprclem  8351  ominf4  8683  canthp1lem2  9020  pwfseqlem4  9029  pwxpndom2  9032  lbioo  11563  ubioo  11564  fzp1disj  11742  fzonel  11817  fzouzdisj  11838  hashbclem  12485  harmonic  13752  eirrlem  14019  ruclem13  14059  prmreclem6  14523  4sqlem17  14563  vdwlem12  14594  vdwnnlem3  14599  mreexmrid  15132  psgnunilem3  16720  efgredlemb  16963  efgredlem  16964  00lss  17783  alexsublem  20710  ptcmplem4  20721  nmoleub2lem3  21764  dvferm1lem  22551  dvferm2lem  22553  plyeq0lem  22773  logno1  23185  lgsval2lem  23779  pntpbnd2  23970  ubico  27820  pm2.65ni  31679  lbioc  31792  bnj1523  34528
  Copyright terms: Public domain W3C validator