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  3789  0nelop  4737  canth  6242  sdom0  7649  canthwdom  8005  cardprclem  8360  ominf4  8692  canthp1lem2  9031  pwfseqlem4  9040  pwxpndom2  9043  lbioo  11560  ubioo  11561  fzp1disj  11738  fzonel  11809  fzouzdisj  11829  hashbclem  12467  harmonic  13633  eirrlem  13798  ruclem13  13836  prmreclem6  14298  4sqlem17  14338  vdwlem12  14369  vdwnnlem3  14374  mreexmrid  14898  psgnunilem3  16327  efgredlemb  16570  efgredlem  16571  00lss  17388  alexsublem  20307  ptcmplem4  20318  nmoleub2lem3  21361  dvferm1lem  22148  dvferm2lem  22150  plyeq0lem  22370  logno1  22773  lgsval2lem  23337  pntpbnd2  23528  ubico  27282  lbioc  31145  fouriersw  31560  bnj1523  33224
  Copyright terms: Public domain W3C validator