Theorem eqeq2 1531

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 1528	. 2 |- (A = B -> (A = C <-> B = C))
2		eqcom 1524	. 2 |- (C = A <-> A = C)
3		eqcom 1524	. 2 |- (C = B <-> B = C)
4	1, 2, 3	3bitr4g 566	1 |- (A = B -> (C = A <-> C = B))

Syntax hints:   -> wi 3   <-> wb 153   = wceq 997

This theorem is referenced by:  eqeq2i 1532  eqeq2d 1533  eqeq12 1534  eleq1 1581  neeq2 1638  eqvinc 1930  alexeq 1932  ceqex 1933  moeq3 1968  mo2icl 1970  moi2 1971  moi 1972  eqif 2429  sneq 2469  preqr1 2535  prel12 2538  dtru 2828  opthg 2844  solin 2913  so 2920  euuni 2938  reuuni2f 2940  dfwe2 2992  ordequn 3137  findsg 3214  tfindsg 3219  ideqg 3333  resieq 3433  funopg 3604  fneq2 3640  foeq3 3727  tz6.12f 3795  tz6.12i 3798  funbrfv 3807  funopfvg 3809  fnbrfvb 3810  funbrfvbg 3814  fvelima 3821  fvopab2 3848  fconst5 3905  f1fvf 3932  f1fveq 3934  isowe 3961  f1oweALT 3964  caoprcan 4113  oawordeu 4247  eceqopreq 4374  2dom 4488  fundmen 4489  nneneq 4577  aceq5 4802  alephfp 4965  cardcf 4976  cfeq0 4979  ltsopq 5140  ltexpq 5145  halfpq 5147  ltsosr 5268  map2psrpr 5285  ltsor 5326  addcan 5417  subval 5422  subaddi 5436  subadd 5440  neg11 5474  mulcant2i 5753  mulcant2iOLD 5754  divvali 5769  divmuli 5770  divmul 5772  divmulOLD 5773  div11 5822  rec11i 5836  redivcli 5856  nnleltp1 6015  nn0ind-raph 6299  sq11 6718  sqeqor 6738  nn0opth2 6758  cru 6828  replim 6851  climuni 7189  efcltlem2 7395  reef11 7500  reeff1olem2 7516  acdc3 7579  acdc5 7585  infpn2 7601  meteq0 7897  dscmet 8003  isgrpi 8127  grpidinv2 8144  isgrp2i 8160  ghgrpilem3 8219  cosh111 8800  efifolem1 8805  efifolem6 8810  hvsubeq0 9018  hvaddcan 9020  hvsubadd 9027  normsub0 9086  hlimunii 9192  occllem5 9260  omlsi 9329  pjoml 9352  nonbooli 9679  pj11 9742  lnopeq 10017  nmopun 10022  rnbra 10123  pjclem4a 10210  pj3lem1 10218  strlem4 10265  hstrlem4 10273  jplem1 10279  superpos 10365  ghomf1olem 10481  fiiu 10535  hmeogrp 10632  usinuniop 10703  cmpida 10789  cmpidb 10790  ishomb 10798  ismonb2 10822  cmpmon 10825  isepib2 10832  iepiclem 10833

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain