Theorem eqeq2 1476

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 1473	. 2 |- (A = B -> (A = C <-> B = C))
2		eqcom 1469	. 2 |- (C = A <-> A = C)
3		eqcom 1469	. 2 |- (C = B <-> B = C)
4	1, 2, 3	3bitr4g 553	1 |- (A = B -> (C = A <-> C = B))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953

This theorem is referenced by:  eqeq2i 1477  eqeq2d 1478  eqeq12 1479  eleq1 1526  neeq2 1583  eqvinc 1874  alexeq 1876  ceqex 1877  moeq3 1912  mo2icl 1914  moi 1915  eqif 2367  sneq 2407  preqr1 2472  prel12 2475  dtru 2762  opthg 2778  ideqgOLD 2825  solin 2848  so 2855  euuni 2871  reuuni2f 2873  dfwe2 2925  ordequn 3070  findsg 3147  tfindsg 3152  ideqg 3266  resieq 3360  funopg 3533  fneq2 3569  foeq3 3655  tz6.12f 3723  tz6.12i 3726  funbrfv 3735  funopfvg 3737  fnbrfvb 3738  funbrfvbg 3742  fvelima 3749  fvopab2 3776  fconst5 3833  f1fvf 3860  f1fveq 3861  isowe 3888  f1oweALT 3891  caoprcan 4041  oawordeu 4173  eceqopreq 4297  2dom 4408  fundmen 4409  nneneq 4492  aceq5 4712  alephfp 4872  cardcf 4883  cfeq0 4886  ltsopq 5047  ltexpq 5052  halfpq 5054  ltsosr 5175  map2psrpr 5192  ltsor 5233  addcant 5324  subvalt 5329  subadd 5343  subaddt 5347  neg11t 5381  mulcant2 5660  divval 5673  divmul 5674  divmult 5676  div11t 5721  rec11 5734  redivcl 5754  nnleltp1t 5901  nn0ind-raph 6162  sq11t 6560  sqeqort 6580  nn0opth2t 6598  crut 6668  replimt 6692  climuni 7036  efcltlem2 7247  reeff1 7350  reeff1olem2 7365  reeff1olem2OLD 7367  acdc3 7429  acdc5 7435  infpn2 7452  meteq0 7751  dscmet 7856  isgrpi 7976  grpidinv2 7994  isgrp2i 8011  ghgrpilem3 8072  cosh111t 8632  efifolem1 8637  efifolem6 8642  hvsubeq0t 8856  hvaddcant 8858  hvsubaddt 8865  normsub0t 8924  hlimuni 9030  occllem5 9093  omls 9161  pjomlt 9184  nonbool 9513  pj11t 9576  lnopeqt 9849  nmopunt 9854  rnbra 9953  pjclem4a 10036  pj3lem1 10044  strlem4 10091  hstrlem4 10099  jplem1 10105  superpos 10189  ghomf1olem 10301  fiiu 10350  hmeogrp 10425  cmpida 10551  cmpidb 10552  ishomb 10560  ismonb2 10582  cmpmon 10585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain