Theorem eqeq2 1487

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 1484	. 2 ⊢ (A = B → (A = C ↔ B = C))
2		eqcom 1480	. 2 ⊢ (C = A ↔ A = C)
3		eqcom 1480	. 2 ⊢ (C = B ↔ B = C)
4	1, 2, 3	3bitr4g 557	1 ⊢ (A = B → (C = A ↔ C = B))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 958

This theorem is referenced by:  eqeq2i 1488  eqeq2d 1489  eqeq12 1490  eleq1 1537  neeq2 1594  eqvinc 1886  alexeq 1888  ceqex 1889  moeq3 1924  mo2icl 1926  moi2 1927  moi 1928  eqif 2381  sneq 2421  preqr1 2485  prel12 2488  dtru 2778  opthg 2794  solin 2863  so 2870  euuni 2887  reuuni2f 2889  dfwe2 2941  ordequn 3086  findsg 3163  tfindsg 3168  ideqg 3282  resieq 3382  funopg 3553  fneq2 3589  foeq3 3676  tz6.12f 3744  tz6.12i 3747  funbrfv 3756  funopfvg 3758  fnbrfvb 3759  funbrfvbg 3763  fvelima 3770  fvopab2 3797  fconst5 3854  f1fvf 3881  f1fveq 3882  isowe 3909  f1oweALT 3912  caoprcan 4061  oawordeu 4195  eceqopreq 4319  2dom 4433  fundmen 4434  nneneq 4518  aceq5 4750  alephfp 4911  cardcf 4923  cfeq0 4926  ltsopq 5087  ltexpq 5092  halfpq 5094  ltsosr 5215  map2psrpr 5232  ltsor 5273  addcant 5364  subvalt 5369  subadd 5383  subaddt 5387  neg11t 5421  mulcant2 5700  mulcant2OLD 5701  divval 5716  divmul 5717  divmult 5719  div11t 5766  rec11 5780  redivcl 5800  nnleltp1t 5956  nn0ind-raph 6216  sq11t 6630  sqeqort 6650  nn0opth2t 6669  crut 6739  replimt 6762  climuni 7099  efcltlem2 7305  reef11t 7409  reeff1olem2 7425  acdc3 7488  acdc5 7494  infpn2 7510  meteq0 7809  dscmet 7915  isgrpi 8039  grpidinv2 8056  isgrp2i 8072  ghgrpilem3 8131  cosh111t 8712  efifolem1 8717  efifolem6 8722  hvsubeq0t 8930  hvaddcant 8932  hvsubaddt 8939  normsub0t 8998  hlimuni 9104  occllem5 9172  omls 9241  pjomlt 9264  nonbool 9591  pj11t 9654  lnopeqt 9929  nmopunt 9934  rnbra 10035  pjclem4a 10121  pj3lem1 10129  strlem4 10176  hstrlem4 10184  jplem1 10190  superpos 10276  ghomf1olem 10391  fiiu 10444  hmeogrp 10524  cmpida 10678  cmpidb 10679  ishomb 10687  ismonb2 10711  cmpmon 10714  isepib2 10721

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain