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

Theorem eqeq2 2292
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 2289 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2285 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2285 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 279 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623
This theorem is referenced by:  eqeq2i  2293  eqeq2d  2294  eqeq12  2295  eleq1  2343  neeq2  2455  alexeq  2897  ceqex  2898  pm13.183  2908  eqeu  2936  moeq3  2942  mo2icl  2944  mob2  2945  euind  2952  reu6i  2956  reuind  2968  sbc2or  2999  sbc5  3015  csbiebg  3120  eqif  3598  sneq  3651  preqr1  3786  prel12  3789  preq12bg  3791  disji2  4010  disjprg  4019  disjxun  4021  dtruALT  4207  dtruALT2  4219  opth  4245  euotd  4267  solin  4337  isso2i  4346  ordequn  4493  tfisi  4649  tfindsg  4651  findsg  4683  ideqg  4835  resieq  4965  cnveqb  5129  cnveq0  5130  iota5  5239  funopg  5286  fneq2  5334  foeq3  5449  tz6.12f  5546  funbrfv  5561  fnbrfvb  5563  fvelimab  5578  fconst5  5731  eufnfv  5752  dff13f  5784  f1fveq  5786  isosolem  5844  f1oweALT  5851  mpt2eq123  5907  ovmpt4g  5970  ov3  5984  ovg  5986  caovcang  6021  caovcan  6024  seqomlem2  6463  oawordeu  6553  omopth  6656  ereq2  6668  qsdisj  6736  eroveu  6753  2dom  6933  fundmen  6934  xpf1o  7023  nneneq  7044  cantnflem1  7391  alephfp  7735  dfac5  7755  cardcf  7878  cfeq0  7882  sornom  7903  fpwwe2cbv  8252  fpwwe2lem3  8255  ltsosr  8716  map2psrpr  8732  axpre-lttri  8787  subval  9043  divval  9426  nn0ind-raph  10112  uzrdgfni  11021  sqeqor  11217  nn0opth2  11287  hashbclem  11390  hashbc  11391  wrdind  11477  sqrval  11722  sqrmo  11737  summolem2  12189  divides  12533  dvdstr  12562  odd2np1lem  12586  ndvdssub  12606  bitsinv1  12633  eucalglt  12755  ramcl2lem  13056  ramcl  13076  imasaddfnlem  13430  posi  14084  orbsta  14767  odlem1  14850  gexlem1  14890  slwispgp  14922  sylow3lem6  14943  efgrelexlemb  15059  gsumval3  15191  pgpfac1  15315  pgpfaclem2  15317  pgpfac  15319  ablfaclem1  15320  isdomn  16035  mvrval  16166  coe1tmmul2  16352  coe1tmmul  16353  obsip  16621  t0sep  17052  t1sep2  17097  is2ndc  17172  kqt0lem  17427  isr0  17428  isufil2  17603  xmeteq0  17903  imasf1oxmet  17939  xrsxmet  18315  iccpnfcnv  18442  dyadmax  18953  dyadmbl  18955  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  mdegle0  19463  fta1g  19553  ig1peu  19557  fta1  19688  aalioulem2  19713  efopn  20005  efrlim  20264  musum  20431  dvdsmulf1o  20434  dchrsum2  20507  sumdchr2  20509  dchrisumlem3  20640  ex-opab  20819  isgrpoi  20865  grpoidinv2  20885  isgrp2d  20902  isgrpda  20964  isexid2  20992  ghgrp  21035  hvsubeq0  21647  hvaddcan  21649  hvsubadd  21656  normsub0  21715  omlsi  21983  pjoml  22015  nonbooli  22230  pj11  22293  lnopeq  22589  nmopun  22594  pjclem4a  22778  pj3lem1  22786  strlem4  22834  hstrlem4  22842  jplem1  22848  superpos  22934  ifeqeqx  23034  xrge0iifcnv  23315  disji2f  23354  disjif2  23358  disjabrex  23359  disjabrexf  23360  esumpr2  23439  subfacp1lem3  23713  pconcn  23755  cnpcon  23761  txpcon  23763  conpcon  23766  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3  23859  snmlflim  23915  ghomf1olem  24001  relexpindlem  24036  sltres  24318  nofulllem5  24360  elfix  24443  axcontlem12  24603  rankeq1o  24801  alexeqd  24962  cbcpcp  25162  prl2  25169  ismnl2  25268  grpodrcan  25375  issubcv  25670  cmpida  25774  cmpidb  25775  ishomb  25788  ismonb2  25812  cmpmon  25815  isepib2  25822  iepiclem  25823  sgplpte22  26138  nn0prpw  26239  f1opr  26391  fdc  26455  istotbnd  26493  ismaxidl  26665  uvcval  27234  unxpwdom3  27256  dgraalem  27350  dgraaub  27353  hashgcdeq  27517  pm13.192  27610  2sbc6g  27615  2sbc5g  27616  pm14.122b  27623  elprchashprn2  28088  frgra3vlem1  28178  3vfriswmgralem  28182  equncomVD  28644  csbingVD  28660  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  relopabVD  28677  bnj1321  29057  lsatcmp  29193  lshpkrlem1  29300  trlval2  30352  cdlemg1cex  30777  cdlemm10N  31308  dicval  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator