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

Theorem pm2.61ine 2682
Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61ine.1  |-  ( A  =  B  ->  ph )
pm2.61ine.2  |-  ( A  =/=  B  ->  ph )
Assertion
Ref Expression
pm2.61ine  |-  ph

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2  |-  ( A  =/=  B  ->  ph )
2 nne 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 195 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 164 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    =/= wne 2601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2603
This theorem is referenced by:  rgenz  3780  raaan  3782  raaanv  3783  iinrab2  4228  iinvdif  4237  riinrab  4241  reusv2lem2  4489  reusv6OLD  4498  reusv7OLD  4499  xpriindi  4971  dmxpid  5054  dmxpss  5264  rnxpid  5266  cnvpo  5370  xpcoid  5373  fnprb  5931  fconstfv  5935  xpexr  6513  frxp  6677  suppimacnv  6696  fodomr  7454  wdompwdom  7785  en3lp  7814  inf3lemd  7825  prdom2  8165  iunfictbso  8276  infpssrlem4  8467  1re  9377  dedekindle  9526  00id  9536  ioorebas  11383  fzfi  11786  hash2prde  12171  repswsymballbi  12410  cshw0  12423  cshwmodn  12424  cshwsublen  12425  cshwn  12426  cshwlen  12428  cshwidx0  12434  cshwsidrepswmod0  14113  cshwshashlem1  14114  cshwshashlem2  14115  cshwsdisj  14117  cntzssv  15837  psgnunilem4  15994  mulmarep1gsum2  18360  plyssc  21643  axsegcon  23124  axpaschlem  23137  axlowdimlem16  23154  axcontlem7  23167  axcontlem8  23168  axcontlem12  23172  usgra2edg  23252  usgrcyclnl2  23478  4cycl4dv  23504  siii  24204  h1de2ctlem  24909  riesz3i  25417  unierri  25459  dya2iocuni  26650  sibf0  26672  dfpo2  27516  cgrextend  27990  ifscgr  28026  idinside  28066  btwnconn1lem12  28080  btwnconn1  28083  linethru  28135  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  sdrgacs  29511  nn0lt2  30139  nn01to3  30140  1to3vfriswmgra  30552  frgranbnb  30565  numclwwlk5  30658  ssnn0fi  30697  zlmodzxznm  30928  ax6e2ndeq  31155  bnj1143  31671  bnj571  31786  bnj594  31792  bnj852  31801  bj-xpnzex  32298
  Copyright terms: Public domain W3C validator