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

Theorem eqeq2 2442
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 2439 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
2 eqcom 2435 . 2  |-  ( C  =  A  <->  A  =  C )
3 eqcom 2435 . 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 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  eqeq2i  2443  eqeq2d  2444  eqeq12  2445  eleq1  2493  neeq2  2607  alexeqg  3077  alexeq  3078  pm13.183  3089  eqeu  3119  moeq3  3125  mo2icl  3127  mob2  3128  euind  3135  reu6i  3139  reuind  3151  sbc2or  3183  sbc5  3199  csbiebg  3299  eqif  3815  sneq  3875  preqr1  4034  prel12  4037  preq12bg  4039  prel12g  4040  disji2  4267  disjprg  4276  dtruALT  4512  dtruALT2  4524  opth  4554  euotd  4580  solin  4651  ordequn  4806  ideqg  4978  resieq  5108  cnveqb  5281  cnveq0  5282  iota5  5389  funopg  5438  fneq2  5488  foeq3  5606  tz6.12f  5696  funbrfv  5718  fnbrfvb  5720  fvelimab  5735  elrnrexdm  5835  fconst5  5922  eufnfv  5938  f1veqaeq  5959  isosolem  6025  mpt2eq123  6134  ovmpt4g  6202  ov3  6216  ovg  6218  caovcang  6253  caovcan  6256  tfisi  6458  tfindsg  6460  findsg  6492  f1oweALT  6550  seqomlem2  6892  oawordeu  6982  omopth  7085  ereq2  7097  qsdisj  7165  eroveu  7183  2dom  7370  fundmen  7371  xpf1o  7461  nneneq  7482  cantnflem1  7885  cantnflem1OLD  7908  alephfp  8266  dfac5  8286  cardcf  8409  cfeq0  8413  sornom  8434  fpwwe2cbv  8784  fpwwe2lem3  8787  ltsosr  9248  map2psrpr  9264  axpre-lttri  9319  subval  9588  divval  9983  nn0ind-raph  10729  uzrdgfni  11764  sqeqor  11963  nn0opth2  12033  elprchashprn2  12139  hash2prde  12162  hash2pwpr  12165  hashbclem  12188  hashbc  12189  wrdind  12354  wrd2ind  12355  sqrval  12709  sqrmo  12724  summolem2  13176  divides  13519  dvdstr  13548  odd2np1lem  13573  ndvdssub  13593  bitsinv1  13620  eucalglt  13742  ramcl2lem  14052  ramcl  14072  cshwrepswhash1  14111  imasaddfnlem  14448  posi  15102  orbsta  15810  symgfvne  15872  symgfix2  15900  odlem1  16017  gexlem1  16057  slwispgp  16089  sylow3lem6  16110  efgrelexlemb  16226  gsumval3OLD  16361  gsumval3lem2  16363  pgpfac1  16554  pgpfaclem2  16556  pgpfac  16558  ablfaclem1  16559  isdomn  17287  mvrval  17427  coe1tmmul2  17626  coe1tmmul  17627  obsip  17987  uvcval  18051  dmatcomp  18144  marrepval  18214  marepvval  18219  minmar1val  18295  gsummatr01  18306  t0sep  18769  t1sep2  18814  is2ndc  18891  kqt0lem  19150  isr0  19151  isufil2  19322  xmeteq0  19754  imasf1oxmet  19791  xrsxmet  20227  iccpnfcnv  20357  dyadmax  20919  dyadmbl  20921  dvfsumle  21334  dvfsumabs  21336  dvfsumlem1  21339  mdegle0  21432  fta1g  21523  ig1peu  21527  fta1  21658  aalioulem2  21683  efopn  21987  efrlim  22247  musum  22415  dvdsmulf1o  22418  dchrsum2  22491  sumdchr2  22493  axtgcgrid  22808  axtgbtwnid  22811  tglowdim1i  22835  axcontlem12  23043  wlkon  23251  wlkntrllem3  23282  spthonepeq  23308  fargshiftf1  23345  constr3trllem2  23359  ex-opab  23461  isgrpoi  23507  grpoidinv2  23527  isgrp2d  23544  isgrpda  23606  isexid2  23634  ghgrp  23677  hvsubeq0  24292  hvaddcan  24294  hvsubadd  24301  normsub0  24360  omlsi  24629  pjoml  24661  nonbooli  24876  pj11  24939  lnopeq  25235  nmopun  25240  pjclem4a  25424  pj3lem1  25432  strlem4  25480  hstrlem4  25488  jplem1  25494  superpos  25580  rmoeq  25694  ifeqeqx  25725  disji2f  25744  disjif2  25748  disjabrex  25749  disjabrexf  25750  disjxpin  25753  disjunsn  25759  ofpreima  25807  fgreu  25813  fcnvgreu  25814  kerf1hrm  26144  xrge0iifcnv  26216  esumpr2  26370  eulerpartlemgvv  26606  eulerpartlemgh  26608  eulerpartlemgs2  26610  sgnsub  26774  plymulx0  26795  subfacp1lem3  26917  pconcn  26960  cnpcon  26966  txpcon  26968  conpcon  26971  cvmlift3lem2  27056  cvmlift3lem4  27058  cvmlift3  27064  snmlflim  27068  ghomf1olem  27159  relexpindlem  27187  iota5f  27227  prodmolem2  27294  sltres  27651  nofulllem5  27693  rankeq1o  28055  fin2so  28257  mblfinlem2  28270  mbfresfi  28279  cnambfre  28281  ftc1anclem8  28315  nn0prpw  28359  f1opr  28459  fdc  28482  istotbnd  28509  ismaxidl  28681  mpt2bi123f  28816  mptbi12f  28820  sbcom3OLD  28821  unxpwdom3  29290  dgraalem  29344  dgraaub  29347  hashgcdeq  29408  pm13.192  29506  2sbc6g  29511  2sbc5g  29512  pm14.122b  29519  hashrabsn1  30076  ccats1rev  30103  usg2wlkeq  30132  wlklniswwlkn2  30177  wwlknredwwlkn  30201  2wlkonot  30227  2spthonot  30228  el2wlkonot  30231  el2spthonot  30232  el2spthonot0  30233  clwwlkn  30273  clwlkisclwwlklem2a4  30289  clwwlkext2edg  30307  clwwnisshclwwn  30316  hashecclwwlkn1  30351  usghashecclwwlk  30352  clwlkfoclwwlk  30361  rusgraprop2  30397  rusgrasn  30400  wwlkextprop  30406  rusgranumwlklem1  30410  rusgranumwlklem2  30411  rusgranumwlklem3  30412  rusgranumwlkg  30419  clwlknclwlkdifs  30421  frgra3vlem1  30435  3vfriswmgralem  30439  usg2spot2nb  30501  usgreg2spot  30503  2spotmdisj  30504  usgreghash2spot  30505  numclwwlkdisj  30516  numclwwlkovf  30517  numclwwlkovg  30523  numclwlk1lem2f1  30530  numclwwlkovq  30535  numclwwlkovh  30537  numclwwlk5  30548  frgrareg  30553  frgraregord013  30554  friendshipgt3  30557  equncomVD  31303  csbingVD  31319  csbsngVD  31328  csbxpgVD  31329  csbresgVD  31330  csbrngVD  31331  csbima12gALTVD  31332  csbunigVD  31333  csbfv12gALTVD  31334  relopabVD  31336  bnj1321  31717  bj-csbsnlem  31996  lsatcmp  32218  lshpkrlem1  32325  trlval2  33377  cdlemg1cex  33802  cdlemm10N  34333  dicval  34391
  Copyright terms: Public domain W3C validator