Theorem eqeq2 1893

Description: Equality implies equivalence of equalities.

Assertion

Ref	Expression
eqeq2	|- (A = B -> (C = A <-> C = B))

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 1890	. 2 |- (A = B -> (A = C <-> B = C))
2		eqcom 1886	. 2 |- (C = A <-> A = C)
3		eqcom 1886	. 2 |- (C = B <-> B = C)
4	1, 2, 3	3bitr4g 614	1 |- (A = B -> (C = A <-> C = B))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298

This theorem is referenced by:  eqeq2i 1894  eqeq2d 1895  eqeq12 1896  eleq1 1957  neeq2 2025  eqvincOLD 2388  alexeq 2390  ceqex 2391  moeq3 2432  mo2icl 2434  moi2 2435  moi 2436  euind 2439  reuind 2450  sbc5g 2470  eqif 3004  sneq 3054  preqr1 3152  prel12 3155  dtruALT 3517  opthg 3533  solin 3612  so 3620  ordequn 3770  euuni 3807  reuuni2f 3810  euexeqOLD 3826  euexaleq 3827  dfwe2OLD 3862  tfindsg 3944  findsg 3980  ideqg 4114  ideqgOLD 4115  resieq 4227  funopg 4454  fneq2 4504  foeq3 4615  tz6.12f 4695  tz6.12i 4698  funbrfv 4709  funopfvg 4711  fnbrfvb 4712  funbrfvbg 4716  fvelimaOLD 4724  fvelimab 4725  fvopab2 4754  eufnfv 4771  fconst5 4824  dff13f 4851  f1fveq 4852  isowe 4880  f1oweALT 4883  caoprcan 4988  reiota2f 5109  oawordeu 5237  eceqopreq 5372  2dom 5486  fundmen 5487  riota5 5580  nneneq 5606  aceq5 5902  alephfp 6048  cardcf 6059  cfeq0 6062  ltsopq 6227  ltexpq 6232  halfpq 6234  ltsosr 6355  map2psrpr 6372  ltsor 6413  addcan 6507  subval 6512  subadd 6532  neg11 6569  mulcant2i 6879  divvali 6893  divmul 6896  div11 6941  rec11i 6954  redivcli 6976  nnleltp1 7138  nn0ind-raph 7426  sq11 7874  sqeqor 7895  nn0opth2 7918  cru 7988  replim 8011  climuni 8359  efcltlem2 8567  reef11 8674  reeff1olem2 8690  acdc3 8755  acdc5 8762  infpn2 8778  meteq0 9089  dscmet 9196  isgrpi 9322  grpidinv2 9344  isgrp2i 9360  ghgrpilem3 9443  cosh111 10071  efifolem1 10076  efifolem6 10081  findcardOLD 10179  txcn 10227  hausfillim 10303  usinuniop 10341  isexid2 10372  hvsubeq0 10567  hvaddcan 10569  hvsubadd 10577  normsub0 10636  hlimunii 10742  occllem5 10810  omlsi 10879  pjoml 10902  nonbooli 11231  pj11 11294  lnopeq 11571  nmopun 11576  rnbra 11678  pjclem4a 11771  pj3lem1 11779  strlem4 11826  hstrlem4 11834  jplem1 11840  superpos 11926  bnj147 12480  bnj1323 13056  fz1eqblem 13608  fz1eqb 13609  ghomf1olem 13637  divides 13664  dvdstr 13687  ndvdssub 13710  axfelem12 14042  axfelem15 14045  axfelem16 14046  brtxp 14067  elfix 14077  fiiu 14344  cnveq2 14455  cnveq3 14456  cbcpcp 14504  cbicplem 14508  prl2 14514  ismnl2 14610  grpdrcan 14738  hmeogrp 14892  invtrgrp 14979  cmpida 15121  cmpidb 15122  ishomb 15137  ismonb2 15161  cmpmon 15164  isepib2 15171  iepiclem 15172  isseg2 15305  eqeu 15351  subtr 15352  subtr2 15353  is2ndc 15472  filfinnfr 15561  isufil2 15565  ufilmax 15568  ufileu 15573  oprabvalg 15706  f1opr 15714  fdc 15812  heiborlem10 15964  heiborlem11 15965  heiborlem13 15967  isgrpda 16033  pcorev 16087  pi1bval 16088  pi1fval 16092  ismaxidl 16188  erdisj3 16266  pm13.183 16373  pm13.192 16374  2sbc6g 16379  2sbc5g 16380  pm14.122b 16387  equncomVD 16692  poslem 16774  isgrpiNEW 17115  grpidinv2NEW 17119

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain