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

Theorem pm2.61ine 3100
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 3020 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61ine.1 . . 3 (𝐴 = 𝐵𝜑)
42, 3sylbi 218 . 2 𝐴𝐵𝜑)
51, 4pm2.61i 183 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  pm2.61ne  3102  pm2.61iine  3107  raaan  4458  raaanv  4459  iinrab2  4984  iinvdif  4994  riinrab  4998  reusv2lem2  5291  po2ne  5483  xpriindi  5701  dmxpid  5794  dmxpss  6022  rnxpid  6024  cnvpo  6132  xpcoid  6135  fnprb  6963  fntpb  6964  xpexr  7611  frxp  7811  suppimacnv  7832  fodomr  8657  wdompwdom  9031  en3lp  9066  inf3lemd  9079  prdom2  9421  iunfictbso  9529  infpssrlem4  9717  1re  10630  dedekindle  10793  00id  10804  nn0lt2  12034  nn01to3  12330  ioorebas  12829  fzfi  13330  ssnn0fi  13343  hash2prde  13818  repswsymballbi  14132  cshw0  14146  cshwmodn  14147  cshwsublen  14148  cshwn  14149  cshwlen  14151  cshwidx0  14158  dmtrclfv  14368  cncongr2  16002  cshwsidrepswmod0  16418  cshwshashlem1  16419  cshwshashlem2  16420  cshwsdisj  16422  cntzssv  18398  psgnunilem4  18556  sdrgacs  19511  mulmarep1gsum2  21113  plyssc  24719  cxpsqrtth  25239  addsqnreup  25947  2sqreultlem  25951  2sqreunnltlem  25954  axsegcon  26641  axpaschlem  26654  axlowdimlem16  26671  axcontlem7  26684  axcontlem8  26685  axcontlem12  26689  umgrislfupgrlem  26835  edglnl  26856  uhgr2edg  26918  1egrvtxdg0  27221  uspgrn2crct  27514  2pthon3v  27650  clwwlknon0  27800  1pthon2v  27860  1to3vfriswmgr  27987  frgrnbnb  28000  numclwwlk5  28095  siii  28558  h1de2ctlem  29260  riesz3i  29767  unierri  29809  dya2iocuni  31441  sibf0  31492  bnj1143  31962  bnj571  32078  bnj594  32084  bnj852  32093  dfpo2  32889  noresle  33098  cgrextend  33367  ifscgr  33403  idinside  33443  btwnconn1lem12  33457  btwnconn1  33460  linethru  33512  bj-xpnzex  34169  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  sn-1ne2  39038  ax6e2ndeq  40773  lighneal  43623  nrhmzr  44042  zlmodzxznm  44450  itsclc0yqe  44646
  Copyright terms: Public domain W3C validator