MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq2 Unicode version

Theorem eqeq2 2396
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqeq2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )

Proof of Theorem eqeq2
StepHypRef Expression
1 eqeq1 2393 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2389 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2389 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 280 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649
This theorem is referenced by:  eqeq2i  2397  eqeq2d  2398  eqeq12  2399  eleq1  2447  neeq2  2559  alexeq  3008  ceqex  3009  pm13.183  3019  eqeu  3048  moeq3  3054  mo2icl  3056  mob2  3057  euind  3064  reu6i  3068  reuind  3080  sbc2or  3112  sbc5  3128  csbiebg  3233  eqif  3715  sneq  3768  preqr1  3914  prel12  3917  preq12bg  3919  disji2  4140  disjprg  4149  dtruALT  4337  dtruALT2  4349  opth  4376  euotd  4398  solin  4467  ordequn  4622  tfisi  4778  tfindsg  4780  findsg  4812  ideqg  4964  resieq  5096  cnveqb  5266  cnveq0  5267  iota5  5378  funopg  5425  fneq2  5475  foeq3  5591  tz6.12f  5689  funbrfv  5704  fnbrfvb  5706  fvelimab  5721  elrnrexdm  5813  fconst5  5888  eufnfv  5911  f1veqaeq  5944  isosolem  6006  f1oweALT  6013  mpt2eq123  6072  ovmpt4g  6135  ov3  6149  ovg  6151  caovcang  6187  caovcan  6190  seqomlem2  6644  oawordeu  6734  omopth  6837  ereq2  6849  qsdisj  6917  eroveu  6935  2dom  7115  fundmen  7116  xpf1o  7205  nneneq  7226  cantnflem1  7578  alephfp  7922  dfac5  7942  cardcf  8065  cfeq0  8069  sornom  8090  fpwwe2cbv  8438  fpwwe2lem3  8441  ltsosr  8902  map2psrpr  8918  axpre-lttri  8973  subval  9229  divval  9612  nn0ind-raph  10302  uzrdgfni  11225  sqeqor  11422  nn0opth2  11492  elprchashprn2  11594  hash2prde  11615  hashbclem  11628  hashbc  11629  wrdind  11718  sqrval  11969  sqrmo  11984  summolem2  12437  divides  12781  dvdstr  12810  odd2np1lem  12834  ndvdssub  12854  bitsinv1  12881  eucalglt  13003  ramcl2lem  13304  ramcl  13324  imasaddfnlem  13680  posi  14334  orbsta  15017  odlem1  15100  gexlem1  15140  slwispgp  15172  sylow3lem6  15193  efgrelexlemb  15309  gsumval3  15441  pgpfac1  15565  pgpfaclem2  15567  pgpfac  15569  ablfaclem1  15570  isdomn  16281  mvrval  16412  coe1tmmul2  16595  coe1tmmul  16596  obsip  16871  t0sep  17310  t1sep2  17355  is2ndc  17430  kqt0lem  17689  isr0  17690  isufil2  17861  xmeteq0  18277  imasf1oxmet  18313  xrsxmet  18711  iccpnfcnv  18840  dyadmax  19357  dyadmbl  19359  dvfsumle  19772  dvfsumabs  19774  dvfsumlem1  19777  mdegle0  19867  fta1g  19957  ig1peu  19961  fta1  20092  aalioulem2  20117  efopn  20416  efrlim  20675  musum  20843  dvdsmulf1o  20846  dchrsum2  20919  sumdchr2  20921  wlkon  21394  wlkntrllem5  21417  fargshiftf1  21472  constr3trllem2  21486  ex-opab  21588  isgrpoi  21634  grpoidinv2  21654  isgrp2d  21671  isgrpda  21733  isexid2  21761  ghgrp  21804  hvsubeq0  22418  hvaddcan  22420  hvsubadd  22427  normsub0  22486  omlsi  22754  pjoml  22786  nonbooli  23001  pj11  23064  lnopeq  23360  nmopun  23365  pjclem4a  23549  pj3lem1  23557  strlem4  23605  hstrlem4  23613  jplem1  23619  superpos  23705  ifeqeqx  23845  disji2f  23863  disjif2  23867  disjabrex  23868  disjabrexf  23869  kerf1hrm  24078  xrge0iifcnv  24123  esumpr2  24254  subfacp1lem3  24647  pconcn  24690  cnpcon  24696  txpcon  24698  conpcon  24701  cvmlift3lem2  24786  cvmlift3lem4  24788  cvmlift3  24794  snmlflim  24798  ghomf1olem  24884  relexpindlem  24918  iota5f  24961  prodmolem2  25040  sltres  25342  nofulllem5  25384  elfix  25467  axcontlem12  25628  rankeq1o  25826  nn0prpw  26017  f1opr  26117  fdc  26140  istotbnd  26169  ismaxidl  26341  uvcval  26903  unxpwdom3  26925  dgraalem  27019  dgraaub  27022  hashgcdeq  27186  pm13.192  27279  2sbc6g  27284  2sbc5g  27285  pm14.122b  27292  frgra3vlem1  27753  3vfriswmgralem  27757  equncomVD  28321  csbingVD  28337  csbsngVD  28346  csbxpgVD  28347  csbresgVD  28348  csbrngVD  28349  csbima12gALTVD  28350  csbunigVD  28351  csbfv12gALTVD  28352  relopabVD  28354  bnj1321  28734  lsatcmp  29118  lshpkrlem1  29225  trlval2  30277  cdlemg1cex  30702  cdlemm10N  31233  dicval  31291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator