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

Theorem eqeq2 2305
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 2302 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2298 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2298 . 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 1632
This theorem is referenced by:  eqeq2i  2306  eqeq2d  2307  eqeq12  2308  eleq1  2356  neeq2  2468  alexeq  2910  ceqex  2911  pm13.183  2921  eqeu  2949  moeq3  2955  mo2icl  2957  mob2  2958  euind  2965  reu6i  2969  reuind  2981  sbc2or  3012  sbc5  3028  csbiebg  3133  eqif  3611  sneq  3664  preqr1  3802  prel12  3805  preq12bg  3807  disji2  4026  disjprg  4035  disjxun  4037  dtruALT  4223  dtruALT2  4235  opth  4261  euotd  4283  solin  4353  isso2i  4362  ordequn  4509  tfisi  4665  tfindsg  4667  findsg  4699  ideqg  4851  resieq  4981  cnveqb  5145  cnveq0  5146  iota5  5255  funopg  5302  fneq2  5350  foeq3  5465  tz6.12f  5562  funbrfv  5577  fnbrfvb  5579  fvelimab  5594  fconst5  5747  eufnfv  5768  dff13f  5800  f1fveq  5802  isosolem  5860  f1oweALT  5867  mpt2eq123  5923  ovmpt4g  5986  ov3  6000  ovg  6002  caovcang  6037  caovcan  6040  seqomlem2  6479  oawordeu  6569  omopth  6672  ereq2  6684  qsdisj  6752  eroveu  6769  2dom  6949  fundmen  6950  xpf1o  7039  nneneq  7060  cantnflem1  7407  alephfp  7751  dfac5  7771  cardcf  7894  cfeq0  7898  sornom  7919  fpwwe2cbv  8268  fpwwe2lem3  8271  ltsosr  8732  map2psrpr  8748  axpre-lttri  8803  subval  9059  divval  9442  nn0ind-raph  10128  uzrdgfni  11037  sqeqor  11233  nn0opth2  11303  hashbclem  11406  hashbc  11407  wrdind  11493  sqrval  11738  sqrmo  11753  summolem2  12205  divides  12549  dvdstr  12578  odd2np1lem  12602  ndvdssub  12622  bitsinv1  12649  eucalglt  12771  ramcl2lem  13072  ramcl  13092  imasaddfnlem  13446  posi  14100  orbsta  14783  odlem1  14866  gexlem1  14906  slwispgp  14938  sylow3lem6  14959  efgrelexlemb  15075  gsumval3  15207  pgpfac1  15331  pgpfaclem2  15333  pgpfac  15335  ablfaclem1  15336  isdomn  16051  mvrval  16182  coe1tmmul2  16368  coe1tmmul  16369  obsip  16637  t0sep  17068  t1sep2  17113  is2ndc  17188  kqt0lem  17443  isr0  17444  isufil2  17619  xmeteq0  17919  imasf1oxmet  17955  xrsxmet  18331  iccpnfcnv  18458  dyadmax  18969  dyadmbl  18971  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  mdegle0  19479  fta1g  19569  ig1peu  19573  fta1  19704  aalioulem2  19729  efopn  20021  efrlim  20280  musum  20447  dvdsmulf1o  20450  dchrsum2  20523  sumdchr2  20525  dchrisumlem3  20656  ex-opab  20835  isgrpoi  20881  grpoidinv2  20901  isgrp2d  20918  isgrpda  20980  isexid2  21008  ghgrp  21051  hvsubeq0  21663  hvaddcan  21665  hvsubadd  21672  normsub0  21731  omlsi  21999  pjoml  22031  nonbooli  22246  pj11  22309  lnopeq  22605  nmopun  22610  pjclem4a  22794  pj3lem1  22802  strlem4  22850  hstrlem4  22858  jplem1  22864  superpos  22950  ifeqeqx  23050  xrge0iifcnv  23330  disji2f  23369  disjif2  23373  disjabrex  23374  disjabrexf  23375  esumpr2  23454  subfacp1lem3  23728  pconcn  23770  cnpcon  23776  txpcon  23778  conpcon  23781  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3  23874  snmlflim  23930  ghomf1olem  24016  relexpindlem  24051  prodmolem2  24158  sltres  24389  nofulllem5  24431  elfix  24514  axcontlem12  24675  rankeq1o  24873  alexeqd  25065  cbcpcp  25265  prl2  25272  ismnl2  25371  grpodrcan  25478  issubcv  25773  cmpida  25877  cmpidb  25878  ishomb  25891  ismonb2  25915  cmpmon  25918  isepib2  25925  iepiclem  25926  sgplpte22  26241  nn0prpw  26342  f1opr  26494  fdc  26558  istotbnd  26596  ismaxidl  26768  uvcval  27337  unxpwdom3  27359  dgraalem  27453  dgraaub  27456  hashgcdeq  27620  pm13.192  27713  2sbc6g  27718  2sbc5g  27719  pm14.122b  27726  f1veqaeq  28188  elprchashprn2  28216  iswlkon  28332  wlkntrllem5  28349  fargshiftf1  28382  constr3trllem2  28397  frgra3vlem1  28424  3vfriswmgralem  28428  equncomVD  28960  csbingVD  28976  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  relopabVD  28993  bnj1321  29373  lsatcmp  29815  lshpkrlem1  29922  trlval2  30974  cdlemg1cex  31399  cdlemm10N  31930  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator