Theorem eqeq2 1482

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 1479	. 2 |- (A = B -> (A = C <-> B = C))
2		eqcom 1475	. 2 |- (C = A <-> A = C)
3		eqcom 1475	. 2 |- (C = B <-> B = C)
4	1, 2, 3	3bitr4g 554	1 |- (A = B -> (C = A <-> C = B))

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

This theorem is referenced by:  eqeq2i 1483  eqeq2d 1484  eqeq12 1485  eleq1 1532  neeq2 1589  eqvinc 1880  alexeq 1882  ceqex 1883  moeq3 1918  mo2icl 1920  moi2 1921  moi 1922  eqif 2374  sneq 2414  preqr1 2478  prel12 2481  dtru 2768  opthg 2784  solin 2853  so 2860  euuni 2877  reuuni2f 2879  dfwe2 2931  ordequn 3076  findsg 3153  tfindsg 3158  ideqg 3272  resieq 3372  funopg 3543  fneq2 3579  foeq3 3665  tz6.12f 3733  tz6.12i 3736  funbrfv 3745  funopfvg 3747  fnbrfvb 3748  funbrfvbg 3752  fvelima 3759  fvopab2 3786  fconst5 3843  f1fvf 3870  f1fveq 3871  isowe 3898  f1oweALT 3901  caoprcan 4050  oawordeu 4182  eceqopreq 4306  2dom 4417  fundmen 4418  nneneq 4501  aceq5 4723  alephfp 4883  cardcf 4894  cfeq0 4897  ltsopq 5058  ltexpq 5063  halfpq 5065  ltsosr 5186  map2psrpr 5203  ltsor 5244  addcant 5335  subvalt 5340  subadd 5354  subaddt 5358  neg11t 5392  mulcant2 5670  divval 5683  divmul 5684  divmult 5686  div11t 5731  rec11 5744  redivcl 5764  nnleltp1t 5911  nn0ind-raph 6172  sq11t 6574  sqeqort 6594  nn0opth2t 6613  crut 6683  replimt 6707  climuni 7052  efcltlem2 7264  reeff1 7367  reeff1olem2 7382  reeff1olem2OLD 7384  acdc3 7446  acdc5 7452  infpn2 7469  meteq0 7772  dscmet 7880  isgrpi 8004  grpidinv2 8022  isgrp2i 8038  ghgrpilem3 8099  cosh111t 8667  efifolem1 8672  efifolem6 8677  hvsubeq0t 8890  hvaddcant 8892  hvsubaddt 8899  normsub0t 8958  hlimuni 9064  occllem5 9132  omls 9201  pjomlt 9224  nonbool 9553  pj11t 9616  lnopeqt 9890  nmopunt 9895  rnbra 9996  pjclem4a 10082  pj3lem1 10090  strlem4 10137  hstrlem4 10145  jplem1 10151  superpos 10237  ghomf1olem 10352  gelsupvalOLD 10376  fiiu 10408  hmeogrp 10484  cmpida 10623  cmpidb 10624  ishomb 10632  ismonb2 10654  cmpmon 10657

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

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

Copyright terms: Public domain