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

Theorem pm2.65i 167
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 114 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 129 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 158 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mto  169  mt2  172  noel  3632  0nelop  4446  canth  6539  sdom0  7239  canthwdom  7547  cardprclem  7866  ominf4  8192  canthp1lem2  8528  pwfseqlem4  8537  pwxpndom2  8540  lbioo  10947  ubioo  10948  fzp1disj  11105  fzonel  11152  fzouzdisj  11169  hashbclem  11701  harmonic  12638  eirrlem  12803  ruclem13  12841  prmreclem6  13289  4sqlem17  13329  vdwlem12  13360  vdwnnlem3  13365  mreexmrid  13868  efgredlemb  15378  efgredlem  15379  00lss  16018  alexsublem  18075  ptcmplem4  18086  nmoleub2lem3  19123  dvferm1lem  19868  dvferm2lem  19870  plyeq0lem  20129  logno1  20527  lgsval2lem  21090  pntpbnd2  21281  ubico  24138  psgnunilem3  27396  bnj1523  29440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator