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

Theorem pm2.65i 165
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 112 . 2  |-  ( ps 
->  -.  ph )
3 pm2.65i.1 . . 3  |-  ( ph  ->  ps )
43con3i 127 . 2  |-  ( -. 
ps  ->  -.  ph )
52, 4pm2.61i 156 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mto  167  mt2  170  noel  3493  0nelop  4293  canth  6336  smo11  6423  sdom0  7036  canthwdom  7338  cardprclem  7657  ackbij1lem16  7906  cfsmolem  7941  ominf4  7983  domtriomlem  8113  konigthlem  8235  canthp1lem2  8320  pwfseqlem4  8329  pwxpndom2  8332  grur1  8487  lbioo  10734  ubioo  10735  fzp1disj  10890  uzdisj  10903  fzonel  10934  fzouzdisj  10949  hashbclem  11437  harmonic  12364  eirrlem  12529  ruclem13  12567  prmreclem6  13015  4sqlem17  13055  vdwlem12  13086  vdwnnlem3  13091  mreexmrid  13594  efgredlemb  15104  efgredlem  15105  00lss  15748  alexsublem  17790  ptcmplem4  17801  nmoleub2lem3  18649  i1f0  19095  itg2const2  19149  dvferm1lem  19384  dvferm2lem  19386  plyeq0lem  19645  logno1  20036  bposlem3  20578  bposlem9  20584  lgsval2lem  20598  pntpbnd1  20788  pntpbnd2  20789  ubico  23285  derangsn  23985  pconcon  24046  heiborlem8  25690  psgnunilem2  26566  psgnunilem3  26567  fnchoice  26848  bnj1523  28612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator