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

Theorem pm2.61ine 3098
 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 (𝐴 = 𝐵𝜑)
pm2.61ine.2 (𝐴𝐵𝜑)
Assertion
Ref Expression
pm2.61ine 𝜑

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2 (𝐴𝐵𝜑)
2 nne 3018 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61ine.1 . . 3 (𝐴 = 𝐵𝜑)
42, 3sylbi 219 . 2 𝐴𝐵𝜑)
51, 4pm2.61i 184 1 𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1530   ≠ wne 3014 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 209  df-ne 3015 This theorem is referenced by:  pm2.61ne  3100  pm2.61iine  3105  raaan  4458  raaanv  4459  iinrab2  4983  iinvdif  4993  riinrab  4997  reusv2lem2  5290  po2ne  5482  xpriindi  5700  dmxpid  5793  dmxpss  6021  rnxpid  6023  cnvpo  6131  xpcoid  6134  fnprb  6963  fntpb  6964  xpexr  7615  frxp  7812  suppimacnv  7833  fodomr  8660  wdompwdom  9034  en3lp  9069  inf3lemd  9082  prdom2  9424  iunfictbso  9532  infpssrlem4  9720  1re  10633  dedekindle  10796  00id  10807  nn0lt2  12037  nn01to3  12333  ioorebas  12831  fzfi  13332  ssnn0fi  13345  hash2prde  13820  repswsymballbi  14134  cshw0  14148  cshwmodn  14149  cshwsublen  14150  cshwn  14151  cshwlen  14153  cshwidx0  14160  dmtrclfv  14370  cncongr2  16004  cshwsidrepswmod0  16420  cshwshashlem1  16421  cshwshashlem2  16422  cshwsdisj  16424  cntzssv  18450  psgnunilem4  18617  sdrgacs  19572  mulmarep1gsum2  21175  plyssc  24782  cxpsqrtth  25304  addsqnreup  26011  2sqreultlem  26015  2sqreunnltlem  26018  axsegcon  26705  axpaschlem  26718  axlowdimlem16  26735  axcontlem7  26748  axcontlem8  26749  axcontlem12  26753  umgrislfupgrlem  26899  edglnl  26920  uhgr2edg  26982  1egrvtxdg0  27285  uspgrn2crct  27578  2pthon3v  27714  clwwlknon0  27864  1pthon2v  27924  1to3vfriswmgr  28051  frgrnbnb  28064  numclwwlk5  28159  siii  28622  h1de2ctlem  29324  riesz3i  29831  unierri  29873  dya2iocuni  31529  sibf0  31580  bnj1143  32050  bnj571  32166  bnj594  32172  bnj852  32181  dfpo2  32979  noresle  33188  cgrextend  33457  ifscgr  33493  idinside  33533  btwnconn1lem12  33547  btwnconn1  33550  linethru  33602  bj-xpnzex  34259  ovoliunnfl  34921  voliunnfl  34923  volsupnfl  34924  sn-1ne2  39143  ax6e2ndeq  40878  lighneal  43761  nrhmzr  44129  zlmodzxznm  44537  itsclc0yqe  44733
 Copyright terms: Public domain W3C validator