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

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

Proof of Theorem eqeq2
StepHypRef Expression
1 eqeq1 2449 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2445 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2445 . 2  |-  ( C  =  B  <->  B  =  C )
41, 2, 33bitr4g 288 1  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  eqeq2i  2453  eqeq2d  2454  eqeq12  2455  eleq1  2503  neeq2OLD  2647  alexeqg  3109  alexeq  3110  pm13.183  3121  eqeu  3151  moeq3  3157  mo2icl  3159  mob2  3160  euind  3167  reu6i  3171  reuind  3183  sbc2or  3216  sbc5  3232  csbiebg  3332  eqif  3848  sneq  3908  preqr1  4067  prel12  4070  preq12bg  4072  prel12g  4073  disji2  4300  disjprg  4309  dtruALT  4545  dtruALT2  4557  opth  4587  euotd  4613  solin  4685  ordequn  4840  ideqg  5012  resieq  5142  cnveqb  5314  cnveq0  5315  iota5  5422  funopg  5471  fneq2  5521  foeq3  5639  tz6.12f  5729  funbrfv  5751  fnbrfvb  5753  fvelimab  5768  elrnrexdm  5868  fconst5  5956  eufnfv  5972  f1veqaeq  5993  isosolem  6059  mpt2eq123  6166  ovmpt4g  6234  ov3  6248  ovg  6250  caovcang  6285  caovcan  6288  tfisi  6490  tfindsg  6492  findsg  6524  f1oweALT  6582  seqomlem2  6927  oawordeu  7015  omopth  7118  ereq2  7130  qsdisj  7198  eroveu  7216  2dom  7403  fundmen  7404  xpf1o  7494  nneneq  7515  cantnflem1  7918  cantnflem1OLD  7941  alephfp  8299  dfac5  8319  cardcf  8442  cfeq0  8446  sornom  8467  fpwwe2cbv  8818  fpwwe2lem3  8821  ltsosr  9282  map2psrpr  9298  axpre-lttri  9353  subval  9622  divval  10017  nn0ind-raph  10763  uzrdgfni  11802  sqeqor  12001  nn0opth2  12071  elprchashprn2  12177  hash2prde  12200  hash2pwpr  12203  hashbclem  12226  hashbc  12227  wrdind  12392  wrd2ind  12393  sqrval  12747  sqrmo  12762  summolem2  13214  divides  13558  dvdstr  13587  odd2np1lem  13612  ndvdssub  13632  bitsinv1  13659  eucalglt  13781  ramcl2lem  14091  ramcl  14111  cshwrepswhash1  14150  imasaddfnlem  14487  posi  15141  orbsta  15852  symgfvne  15914  symgfix2  15942  odlem1  16059  gexlem1  16099  slwispgp  16131  sylow3lem6  16152  efgrelexlemb  16268  gsumval3OLD  16403  gsumval3lem2  16405  pgpfac1  16603  pgpfaclem2  16605  pgpfac  16607  ablfaclem1  16608  isdomn  17388  mvrval  17516  coe1tmmul2  17751  coe1tmmul  17752  obsip  18168  uvcval  18232  dmatcomp  18325  marrepval  18395  marepvval  18400  minmar1val  18476  gsummatr01  18487  t0sep  18950  t1sep2  18995  is2ndc  19072  kqt0lem  19331  isr0  19332  isufil2  19503  xmeteq0  19935  imasf1oxmet  19972  xrsxmet  20408  iccpnfcnv  20538  dyadmax  21100  dyadmbl  21102  dvfsumle  21515  dvfsumabs  21517  dvfsumlem1  21520  mdegle0  21570  fta1g  21661  ig1peu  21665  fta1  21796  aalioulem2  21821  efopn  22125  efrlim  22385  musum  22553  dvdsmulf1o  22556  dchrsum2  22629  sumdchr2  22631  axtgcgrid  22946  axtgbtwnid  22949  tglowdim1i  22976  axcontlem12  23243  wlkon  23451  wlkntrllem3  23482  spthonepeq  23508  fargshiftf1  23545  constr3trllem2  23559  ex-opab  23661  isgrpoi  23707  grpoidinv2  23727  isgrp2d  23744  isgrpda  23806  isexid2  23834  ghgrp  23877  hvsubeq0  24492  hvaddcan  24494  hvsubadd  24501  normsub0  24560  omlsi  24829  pjoml  24861  nonbooli  25076  pj11  25139  lnopeq  25435  nmopun  25440  pjclem4a  25624  pj3lem1  25632  strlem4  25680  hstrlem4  25688  jplem1  25694  superpos  25780  rmoeq  25893  ifeqeqx  25924  disji2f  25943  disjif2  25947  disjabrex  25948  disjabrexf  25949  disjxpin  25952  disjunsn  25958  ofpreima  26006  fgreu  26012  fcnvgreu  26013  xrge0iifcnv  26385  esumpr2  26539  eulerpartlemgvv  26781  eulerpartlemgh  26783  eulerpartlemgs2  26785  sgnsub  26949  plymulx0  26970  subfacp1lem3  27092  pconcn  27135  cnpcon  27141  txpcon  27143  conpcon  27146  cvmlift3lem2  27231  cvmlift3lem4  27233  cvmlift3  27239  snmlflim  27243  ghomf1olem  27335  relexpindlem  27363  iota5f  27403  prodmolem2  27470  sltres  27827  nofulllem5  27869  rankeq1o  28231  fin2so  28442  mblfinlem2  28455  mbfresfi  28464  cnambfre  28466  ftc1anclem8  28500  nn0prpw  28544  f1opr  28644  fdc  28667  istotbnd  28694  ismaxidl  28866  mpt2bi123f  29001  mptbi12f  29005  unxpwdom3  29474  dgraalem  29528  dgraaub  29531  hashgcdeq  29592  pm13.192  29690  2sbc6g  29695  2sbc5g  29696  pm14.122b  29703  hashrabsn1  30259  ccats1rev  30286  usg2wlkeq  30315  wlklniswwlkn2  30360  wwlknredwwlkn  30384  2wlkonot  30410  2spthonot  30411  el2wlkonot  30414  el2spthonot  30415  el2spthonot0  30416  clwwlkn  30456  clwlkisclwwlklem2a4  30472  clwwlkext2edg  30490  clwwnisshclwwn  30499  hashecclwwlkn1  30534  usghashecclwwlk  30535  clwlkfoclwwlk  30544  rusgraprop2  30580  rusgrasn  30583  wwlkextprop  30589  rusgranumwlklem1  30593  rusgranumwlklem2  30594  rusgranumwlklem3  30595  rusgranumwlkg  30602  clwlknclwlkdifs  30604  frgra3vlem1  30618  3vfriswmgralem  30622  usg2spot2nb  30684  usgreg2spot  30686  2spotmdisj  30687  usgreghash2spot  30688  numclwwlkdisj  30699  numclwwlkovf  30700  numclwwlkovg  30706  numclwlk1lem2f1  30713  numclwwlkovq  30718  numclwwlkovh  30720  numclwwlk5  30731  frgrareg  30736  frgraregord013  30737  friendshipgt3  30740  mat1dimid  30909  scmatid  30921  scmatsubcl  30923  scmatmulcl  30925  equncomVD  31700  csbingVD  31716  csbsngVD  31725  csbxpgVD  31726  csbresgVD  31727  csbrngVD  31728  csbima12gALTVD  31729  csbunigVD  31730  csbfv12gALTVD  31731  relopabVD  31733  bnj1321  32114  bj-csbsnlem  32501  lsatcmp  32744  lshpkrlem1  32851  trlval2  33903  cdlemg1cex  34328  cdlemm10N  34859  dicval  34917
  Copyright terms: Public domain W3C validator