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

Theorem eqeq2 2444
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 2441 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2437 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2437 . 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 1652
This theorem is referenced by:  eqeq2i  2445  eqeq2d  2446  eqeq12  2447  eleq1  2495  neeq2  2607  alexeq  3057  ceqex  3058  pm13.183  3068  eqeu  3097  moeq3  3103  mo2icl  3105  mob2  3106  euind  3113  reu6i  3117  reuind  3129  sbc2or  3161  sbc5  3177  csbiebg  3282  eqif  3764  sneq  3817  preqr1  3964  prel12  3967  preq12bg  3969  disji2  4191  disjprg  4200  dtruALT  4388  dtruALT2  4400  opth  4427  euotd  4449  solin  4518  ordequn  4674  tfisi  4830  tfindsg  4832  findsg  4864  ideqg  5016  resieq  5148  cnveqb  5318  cnveq0  5319  iota5  5430  funopg  5477  fneq2  5527  foeq3  5643  tz6.12f  5741  funbrfv  5757  fnbrfvb  5759  fvelimab  5774  elrnrexdm  5866  fconst5  5941  eufnfv  5964  f1veqaeq  5997  isosolem  6059  f1oweALT  6066  mpt2eq123  6125  ovmpt4g  6188  ov3  6202  ovg  6204  caovcang  6240  caovcan  6243  seqomlem2  6700  oawordeu  6790  omopth  6893  ereq2  6905  qsdisj  6973  eroveu  6991  2dom  7171  fundmen  7172  xpf1o  7261  nneneq  7282  cantnflem1  7637  alephfp  7981  dfac5  8001  cardcf  8124  cfeq0  8128  sornom  8149  fpwwe2cbv  8497  fpwwe2lem3  8500  ltsosr  8961  map2psrpr  8977  axpre-lttri  9032  subval  9289  divval  9672  nn0ind-raph  10362  uzrdgfni  11290  sqeqor  11487  nn0opth2  11557  elprchashprn2  11659  hash2prde  11680  hashbclem  11693  hashbc  11694  wrdind  11783  sqrval  12034  sqrmo  12049  summolem2  12502  divides  12846  dvdstr  12875  odd2np1lem  12899  ndvdssub  12919  bitsinv1  12946  eucalglt  13068  ramcl2lem  13369  ramcl  13389  imasaddfnlem  13745  posi  14399  orbsta  15082  odlem1  15165  gexlem1  15205  slwispgp  15237  sylow3lem6  15258  efgrelexlemb  15374  gsumval3  15506  pgpfac1  15630  pgpfaclem2  15632  pgpfac  15634  ablfaclem1  15635  isdomn  16346  mvrval  16477  coe1tmmul2  16660  coe1tmmul  16661  obsip  16940  t0sep  17380  t1sep2  17425  is2ndc  17501  kqt0lem  17760  isr0  17761  isufil2  17932  xmeteq0  18360  imasf1oxmet  18397  xrsxmet  18832  iccpnfcnv  18961  dyadmax  19482  dyadmbl  19484  dvfsumle  19897  dvfsumabs  19899  dvfsumlem1  19902  mdegle0  19992  fta1g  20082  ig1peu  20086  fta1  20217  aalioulem2  20242  efopn  20541  efrlim  20800  musum  20968  dvdsmulf1o  20971  dchrsum2  21044  sumdchr2  21046  wlkon  21522  wlkntrllem3  21553  spthonepeq  21579  fargshiftf1  21616  constr3trllem2  21630  ex-opab  21732  isgrpoi  21778  grpoidinv2  21798  isgrp2d  21815  isgrpda  21877  isexid2  21905  ghgrp  21948  hvsubeq0  22562  hvaddcan  22564  hvsubadd  22571  normsub0  22630  omlsi  22898  pjoml  22930  nonbooli  23145  pj11  23208  lnopeq  23504  nmopun  23509  pjclem4a  23693  pj3lem1  23701  strlem4  23749  hstrlem4  23757  jplem1  23763  superpos  23849  ifeqeqx  23993  disji2f  24011  disjif2  24015  disjabrex  24016  disjabrexf  24017  disjxpin  24020  ofpreima  24073  kerf1hrm  24254  xrge0iifcnv  24311  esumpr2  24450  subfacp1lem3  24860  pconcn  24903  cnpcon  24909  txpcon  24911  conpcon  24914  cvmlift3lem2  24999  cvmlift3lem4  25001  cvmlift3  25007  snmlflim  25011  ghomf1olem  25097  relexpindlem  25131  iota5f  25174  prodmolem2  25253  sltres  25611  nofulllem5  25653  axcontlem12  25906  rankeq1o  26104  mblfinlem  26234  mbfresfi  26243  cnambfre  26245  ftc1anclem8  26277  nn0prpw  26317  f1opr  26417  fdc  26440  istotbnd  26469  ismaxidl  26641  uvcval  27202  unxpwdom3  27224  dgraalem  27318  dgraaub  27321  hashgcdeq  27485  pm13.192  27578  2sbc6g  27583  2sbc5g  27584  pm14.122b  27591  cshw1v  28239  cshwssizesame  28251  2wlkonot  28285  2spthonot  28286  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  frgra3vlem1  28327  3vfriswmgralem  28331  usg2spot2nb  28391  usgreg2spot  28393  2spotmdisj  28394  usgreghash2spot  28395  equncomVD  28917  csbingVD  28933  csbsngVD  28942  csbxpgVD  28943  csbresgVD  28944  csbrngVD  28945  csbima12gALTVD  28946  csbunigVD  28947  csbfv12gALTVD  28948  relopabVD  28950  bnj1321  29333  lsatcmp  29738  lshpkrlem1  29845  trlval2  30897  cdlemg1cex  31322  cdlemm10N  31853  dicval  31911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator