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 3025
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 2944 . . 3 𝐴𝐵𝐴 = 𝐵)
3 pm2.61ine.1 . . 3 (𝐴 = 𝐵𝜑)
42, 3sylbi 216 . 2 𝐴𝐵𝜑)
51, 4pm2.61i 182 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2940
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 206  df-ne 2941
This theorem is referenced by:  pm2.61ne  3027  pm2.61dne  3028  pm2.61iine  3032  raaan  4479  raaanv  4480  iinrab2  5031  iinvdif  5041  riinrab  5045  reusv2lem2  5355  po2ne  5562  xpriindi  5793  dmxpid  5886  dmxpss  6124  rnxpid  6126  cnvpo  6240  xpcoid  6243  dfpo2  6249  fnprb  7159  fntpb  7160  xpexr  7856  frxp  8059  suppimacnv  8106  fodomr  9075  wdompwdom  9519  en3lp  9555  inf3lemd  9568  prdom2  9947  iunfictbso  10055  infpssrlem4  10247  1re  11160  dedekindle  11324  00id  11335  nn0lt2  12571  nn01to3  12871  ioorebas  13374  fzfi  13883  ssnn0fi  13896  hash2prde  14375  repswsymballbi  14674  cshw0  14688  cshwmodn  14689  cshwsublen  14690  cshwn  14691  cshwlen  14693  cshwidx0  14700  dmtrclfv  14909  cncongr2  16549  cshwsidrepswmod0  16972  cshwshashlem1  16973  cshwshashlem2  16974  cshwsdisj  16976  cntzssv  19113  psgnunilem4  19284  sdrgacs  20282  mulmarep1gsum2  21939  plyssc  25577  cxpsqrtth  26100  addsqnreup  26807  2sqreultlem  26811  2sqreunnltlem  26814  noresle  27061  axsegcon  27918  axpaschlem  27931  axlowdimlem16  27948  axcontlem7  27961  axcontlem8  27962  axcontlem12  27966  umgrislfupgrlem  28115  edglnl  28136  uhgr2edg  28198  1egrvtxdg0  28501  uspgrn2crct  28795  2pthon3v  28930  clwwlknon0  29079  1pthon2v  29139  1to3vfriswmgr  29266  frgrnbnb  29279  numclwwlk5  29374  siii  29837  h1de2ctlem  30539  riesz3i  31046  unierri  31088  dya2iocuni  32940  sibf0  32991  bnj1143  33459  bnj571  33575  bnj594  33581  bnj852  33590  cgrextend  34639  ifscgr  34675  idinside  34715  btwnconn1lem12  34729  btwnconn1  34732  linethru  34784  bj-xpnzex  35476  ovoliunnfl  36166  voliunnfl  36168  volsupnfl  36169  sn-1ne2  40824  cantnfresb  41702  ax6e2ndeq  42929  lighneal  45889  nrhmzr  46257  zlmodzxznm  46664  itsclc0yqe  46933
  Copyright terms: Public domain W3C validator