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

Theorem eqeq2 2413
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 2410 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2406 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2406 . 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  2414  eqeq2d  2415  eqeq12  2416  eleq1  2464  neeq2  2576  alexeq  3025  ceqex  3026  pm13.183  3036  eqeu  3065  moeq3  3071  mo2icl  3073  mob2  3074  euind  3081  reu6i  3085  reuind  3097  sbc2or  3129  sbc5  3145  csbiebg  3250  eqif  3732  sneq  3785  preqr1  3932  prel12  3935  preq12bg  3937  disji2  4159  disjprg  4168  dtruALT  4356  dtruALT2  4368  opth  4395  euotd  4417  solin  4486  ordequn  4641  tfisi  4797  tfindsg  4799  findsg  4831  ideqg  4983  resieq  5115  cnveqb  5285  cnveq0  5286  iota5  5397  funopg  5444  fneq2  5494  foeq3  5610  tz6.12f  5708  funbrfv  5724  fnbrfvb  5726  fvelimab  5741  elrnrexdm  5833  fconst5  5908  eufnfv  5931  f1veqaeq  5964  isosolem  6026  f1oweALT  6033  mpt2eq123  6092  ovmpt4g  6155  ov3  6169  ovg  6171  caovcang  6207  caovcan  6210  seqomlem2  6667  oawordeu  6757  omopth  6860  ereq2  6872  qsdisj  6940  eroveu  6958  2dom  7138  fundmen  7139  xpf1o  7228  nneneq  7249  cantnflem1  7601  alephfp  7945  dfac5  7965  cardcf  8088  cfeq0  8092  sornom  8113  fpwwe2cbv  8461  fpwwe2lem3  8464  ltsosr  8925  map2psrpr  8941  axpre-lttri  8996  subval  9253  divval  9636  nn0ind-raph  10326  uzrdgfni  11253  sqeqor  11450  nn0opth2  11520  elprchashprn2  11622  hash2prde  11643  hashbclem  11656  hashbc  11657  wrdind  11746  sqrval  11997  sqrmo  12012  summolem2  12465  divides  12809  dvdstr  12838  odd2np1lem  12862  ndvdssub  12882  bitsinv1  12909  eucalglt  13031  ramcl2lem  13332  ramcl  13352  imasaddfnlem  13708  posi  14362  orbsta  15045  odlem1  15128  gexlem1  15168  slwispgp  15200  sylow3lem6  15221  efgrelexlemb  15337  gsumval3  15469  pgpfac1  15593  pgpfaclem2  15595  pgpfac  15597  ablfaclem1  15598  isdomn  16309  mvrval  16440  coe1tmmul2  16623  coe1tmmul  16624  obsip  16903  t0sep  17342  t1sep2  17387  is2ndc  17462  kqt0lem  17721  isr0  17722  isufil2  17893  xmeteq0  18321  imasf1oxmet  18358  xrsxmet  18793  iccpnfcnv  18922  dyadmax  19443  dyadmbl  19445  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  mdegle0  19953  fta1g  20043  ig1peu  20047  fta1  20178  aalioulem2  20203  efopn  20502  efrlim  20761  musum  20929  dvdsmulf1o  20932  dchrsum2  21005  sumdchr2  21007  wlkon  21483  wlkntrllem3  21514  spthonepeq  21540  fargshiftf1  21577  constr3trllem2  21591  ex-opab  21693  isgrpoi  21739  grpoidinv2  21759  isgrp2d  21776  isgrpda  21838  isexid2  21866  ghgrp  21909  hvsubeq0  22523  hvaddcan  22525  hvsubadd  22532  normsub0  22591  omlsi  22859  pjoml  22891  nonbooli  23106  pj11  23169  lnopeq  23465  nmopun  23470  pjclem4a  23654  pj3lem1  23662  strlem4  23710  hstrlem4  23718  jplem1  23724  superpos  23810  ifeqeqx  23954  disji2f  23972  disjif2  23976  disjabrex  23977  disjabrexf  23978  disjxpin  23981  ofpreima  24034  kerf1hrm  24215  xrge0iifcnv  24272  esumpr2  24411  subfacp1lem3  24821  pconcn  24864  cnpcon  24870  txpcon  24872  conpcon  24875  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3  24968  snmlflim  24972  ghomf1olem  25058  relexpindlem  25092  iota5f  25135  prodmolem2  25214  sltres  25532  nofulllem5  25574  elfix  25657  axcontlem12  25818  rankeq1o  26016  mblfinlem  26143  mbfresfi  26152  cnambfre  26154  nn0prpw  26216  f1opr  26316  fdc  26339  istotbnd  26368  ismaxidl  26540  uvcval  27102  unxpwdom3  27124  dgraalem  27218  dgraaub  27221  hashgcdeq  27385  pm13.192  27478  2sbc6g  27483  2sbc5g  27484  pm14.122b  27491  2wlkonot  28062  2spthonot  28063  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  frgra3vlem1  28104  3vfriswmgralem  28108  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  usgreghash2spot  28172  equncomVD  28689  csbingVD  28705  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbima12gALTVD  28718  csbunigVD  28719  csbfv12gALTVD  28720  relopabVD  28722  bnj1321  29102  lsatcmp  29486  lshpkrlem1  29593  trlval2  30645  cdlemg1cex  31070  cdlemm10N  31601  dicval  31659
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator