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

Theorem neeq1 2840
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21neeq1d 2837 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wne 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599  df-ne 2778
This theorem is referenced by:  nelrdva  3380  psseq1  3652  0inp0  4755  nnullss  4848  opeqex  4878  fri  4987  frsn  5099  xp11  5471  limeq  5635  tz6.12i  6106  fveqressseq  6245  fprg  6302  tpres  6346  f1dom3el3dif  6401  f1prex  6414  isofrlem  6465  f1oweALT  7017  frxp  7148  suppimacnv  7167  elqsn0  7677  frfi  8064  fiint  8096  marypha1lem  8196  dfac8alem  8709  dfac8clem  8712  aceq3lem  8800  dfac5lem3  8805  dfac5lem4  8806  dfac5  8808  dfac2  8810  dfac9  8815  kmlem1  8829  kmlem12  8840  kmlem14  8842  fin2i  8974  isfin2-2  8998  fin23lem21  9018  fin1a2lem10  9088  axcc2lem  9115  dominf  9124  ac5b  9157  zornn0g  9184  axdclem  9198  dominfac  9248  elwina  9361  elina  9362  iswun  9379  rankcf  9452  axrrecex  9837  elimne0  9883  1re  9892  recex  10505  uzn0  11532  qreccl  11637  xrnemnf  11785  xrnepnf  11786  fztpval  12224  expcl2lem  12686  hashnemnf  12943  hashneq0  12965  hashge2el2difr  13065  relexp1g  13557  ntrivcvgn0  14412  ntrivcvgmullem  14415  fprodntriv  14454  divalglem7  14903  divalg  14907  gcdcllem1  15002  gcdcllem3  15004  isprm2lem  15175  pcpre1  15328  pcqmul  15339  pcqcl  15342  prmgaplem3  15538  prmgaplem4  15539  xpscfv  15988  xpsfrnel  15989  mreintcl  16021  isdrs  16700  isipodrs  16927  sgrp2rid2ex  17180  frgpuptinv  17950  isdrngrd  18539  isnzr2  19027  psgnodpmr  19697  lindfrn  19918  dmatelnd  20060  dmatmul  20061  mdetdiaglem  20162  mdetunilem1  20176  fvmptnn04ifa  20413  chfacfscmulgsum  20423  chfacfpmmulgsum  20427  fiinopn  20470  hausnei  20881  dfcon2  20971  2ndcdisj  21008  regr1lem2  21292  isfbas  21382  ioorinv  23064  ioorcl  23065  vitalilem2  23098  vitalilem3  23099  vitali  23102  itg1climres  23201  mbfi1fseqlem4  23205  dvferm1lem  23465  dvferm2lem  23467  isuc1p  23618  ismon1p  23620  ply1remlem  23640  plydivlem4  23769  aannenlem1  23801  aannenlem2  23802  lgsne0  24774  lgsqr  24790  axtg5seg  25078  axtgupdim2  25084  axtgeucl  25085  axlowdim1  25554  usgranloopv  25670  usgra1v  25682  cusgrafilem2  25771  wlkn0  25818  2pthoncl  25896  iswwlk  25974  eupath2lem2  26268  eupath2lem3  26269  3cyclfrgrarn1  26302  4cycl2vnunb  26307  frgrawopreglem3  26336  norm1exi  27294  shintcl  27376  chintcl  27378  chne0  27540  elspansn2  27613  eigre  27881  eigorth  27884  kbpj  28002  superpos  28400  hatomic  28406  xrge0iifhom  29114  xrge0iif1  29115  esumpr2  29259  sibfof  29532  signswn0  29766  signswch  29767  signstfvneq0  29778  axtgupdim2OLD  29802  bnj168  29855  bnj970  30074  bnj1154  30124  subfacp1lem1  30218  erdszelem8  30237  indispcon  30273  cvmsss2  30313  nepss  30657  frmin  30786  elwlim  30816  elwlimOLD  30817  dfrdg4  31031  fvray  31221  linedegen  31223  fvline  31224  hilbert1.1  31234  rankeq1o  31251  unblimceq0lem  31470  knoppndvlem21  31496  poimirlem1  32380  poimirlem17  32396  poimirlem20  32399  poimirlem32  32411  itg2addnclem3  32433  neificl  32519  isdrngo3  32728  ispridl  32803  ismaxidl  32809  islshp  33084  lsatn0  33104  lshpset2N  33224  atlex  33421  hlsuprexch  33485  3dimlem1  33562  llni2  33616  lplni2  33641  2llnjN  33671  lvoli2  33685  2lplnj  33724  islinei  33844  lnatexN  33883  llnexchb2  33973  lhpmatb  34135  cdleme40m  34573  cdlemftr3  34671  cdlemk28-3  35014  cdlemk35s  35043  cdlemk39s  35045  cdlemk42  35047  dnnumch1  36432  aomclem3  36444  aomclem8  36449  dfac11  36450  dfacbasgrp  36497  ax6e2ndeq  37596  ax6e2ndeqVD  37967  fnchoice  38011  fiiuncl  38059  disjrnmpt2  38170  idlimc  38494  limcperiod  38496  limclner  38519  fperdvper  38609  stoweidlem35  38729  stoweidlem43  38737  stoweidlem59  38753  fourierdlem76  38876  etransclem47  38975  nnfoctbdjlem  39149  elprneb  39741  n0snor2el  40120  funopsn  40141  xnn0nemnf  40208  xnn0n0n1ge2b  40215  structgrssvtxlem  40255  lpvtx  40289  umgrnloopv  40330  usgrnloopvALT  40427  umgrvad2edg  40439  cusgrfilem2  40671  pthdlem2lem  40972  iswwlks  41038  iswwlksnx  41041  2pthdlem1  41136  isclwwlks  41187  3pthdlem1  41330  upgr3v3e3cycl  41346  upgr4cycl4dv4e  41351  eupth2lem2  41386  eupth2lem3lem4  41398  eupth2lem3lem6  41400  3cyclfrgrrn1  41454  4cycl2vnunb-av  41459  frgrwopreglem3  41482  av-frgrareg  41547  nrhmzr  41662
  Copyright terms: Public domain W3C validator