Theorem eqeq2 2241

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq2	⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 2238	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2233	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2233	. 2 ⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶)
4	1, 2, 3	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqeq2i  2242  eqeq2d  2243  eqeq12  2244  eleq1  2294  neeq2  2416  alexeq  2932  ceqex  2933  pm13.183  2944  eqeu  2976  mo2icl  2985  mob2  2986  euind  2993  reu6i  2997  reuind  3011  sbc5  3055  csbiebg  3170  sneq  3680  preqr1g  3849  preqr1  3851  prel12  3854  preq12bg  3856  opth  4329  euotd  4347  ordtriexmid  4619  ontriexmidim  4620  wetriext  4675  tfisi  4685  ideqg  4881  resieq  5023  cnveqb  5192  cnveq0  5193  iota5  5308  funopg  5360  fneq2  5419  foeq3  5557  tz6.12f  5668  funbrfv  5682  fnbrfvb  5684  fvelimab  5702  elrnrexdm  5786  eufnfv  5885  f1veqaeq  5910  mpoeq123  6080  ovmpt4g  6144  ovi3  6159  ovg  6161  caovcang  6184  caovcan  6187  uchoice  6300  frecabcl  6565  nntri3or  6661  dcdifsnid  6672  nnaordex  6696  nnawordex  6697  ereq2  6710  eroveu  6795  2dom  6980  fundmen  6981  xpf1o  7030  nneneq  7043  tridc  7089  elssdc  7094  eqsndc  7095  prfidceq  7120  tpfidceq  7122  fisseneq  7127  fidcenumlemrks  7152  supsnti  7204  isotilem  7205  updjud  7281  nninfwlpoimlemdc  7376  exmidontriimlem3  7438  exmidontriimlem4  7439  onntri35  7455  exmidapne  7479  nqtri3or  7616  ltexnqq  7628  aptisr  7999  srpospr  8003  map2psrprg  8025  axpre-apti  8105  nntopi  8114  subval  8371  eqord1  8663  divvalap  8854  nn0ind-raph  9597  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  wrdind  11307  wrd2ind  11308  reuccatpfxs1lem  11331  sqrtrval  11565  summodclem2  11948  prodmodclem2  12143  divides  12355  dvdstr  12394  odd2np1lem  12438  ndvdssub  12496  bitsinv1  12528  eucalglt  12634  hashgcdeq  12817  ennnfonelemim  13050  imasaddfnlemg  13402  dfgrp2  13615  grpidinv  13647  dfgrp3mlem  13686  isdomn  14289  xmeteq0  15089  mpodvdsmulf1o  15720  gausslemma2dlem0i  15792  upgredgpr  16006  ushgredgedg  16083  ushgredgedgloop  16085  uspgr2wlkeq  16222  clwwlkng  16262  clwwlkext2edg  16279  clwwlknon  16286  clwwlk0on0  16288  pw1dceq  16631  trilpo  16673  trirec0  16674  redcwlpo  16686  redc0  16688  reap0  16689