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  3459  0nelop  4256  canth  6294  smo11  6381  sdom0  6993  canthwdom  7293  cardprclem  7612  ackbij1lem16  7861  cfsmolem  7896  ominf4  7938  domtriomlem  8068  konigthlem  8190  canthp1lem2  8275  pwfseqlem4  8284  pwxpndom2  8287  grur1  8442  lbioo  10687  ubioo  10688  fzp1disj  10843  uzdisj  10856  fzonel  10887  fzouzdisj  10902  hashbclem  11390  harmonic  12317  eirrlem  12482  ruclem13  12520  prmreclem6  12968  4sqlem17  13008  vdwlem12  13039  vdwnnlem3  13044  mreexmrid  13545  efgredlemb  15055  efgredlem  15056  00lss  15699  alexsublem  17738  ptcmplem4  17749  nmoleub2lem3  18596  i1f0  19042  itg2const2  19096  dvferm1lem  19331  dvferm2lem  19333  plyeq0lem  19592  logno1  19983  bposlem3  20525  bposlem9  20531  lgsval2lem  20545  pntpbnd1  20735  pntpbnd2  20736  ubico  23268  derangsn  23701  pconcon  23762  heiborlem8  26542  psgnunilem2  27418  psgnunilem3  27419  fnchoice  27700  bnj1523  29101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator