Theorem eqeq2 2239

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 2236	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2231	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2231	. 2 ⊢ (𝐶 = 𝐵 ↔ 𝐵 = 𝐶)
4	1, 2, 3	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeq2i  2240  eqeq2d  2241  eqeq12  2242  eleq1  2292  neeq2  2414  alexeq  2930  ceqex  2931  pm13.183  2942  eqeu  2974  mo2icl  2983  mob2  2984  euind  2991  reu6i  2995  reuind  3009  sbc5  3053  csbiebg  3168  sneq  3678  preqr1g  3847  preqr1  3849  prel12  3852  preq12bg  3854  opth  4327  euotd  4345  ordtriexmid  4617  ontriexmidim  4618  wetriext  4673  tfisi  4683  ideqg  4879  resieq  5021  cnveqb  5190  cnveq0  5191  iota5  5306  funopg  5358  fneq2  5416  foeq3  5554  tz6.12f  5664  funbrfv  5678  fnbrfvb  5680  fvelimab  5698  elrnrexdm  5782  eufnfv  5880  f1veqaeq  5905  mpoeq123  6075  ovmpt4g  6139  ovi3  6154  ovg  6156  caovcang  6179  caovcan  6182  uchoice  6295  frecabcl  6560  nntri3or  6656  dcdifsnid  6667  nnaordex  6691  nnawordex  6692  ereq2  6705  eroveu  6790  2dom  6975  fundmen  6976  xpf1o  7025  nneneq  7038  tridc  7082  elssdc  7087  eqsndc  7088  prfidceq  7113  tpfidceq  7115  fisseneq  7119  fidcenumlemrks  7143  supsnti  7195  isotilem  7196  updjud  7272  nninfwlpoimlemdc  7367  exmidontriimlem3  7428  exmidontriimlem4  7429  onntri35  7445  exmidapne  7469  nqtri3or  7606  ltexnqq  7618  aptisr  7989  srpospr  7993  map2psrprg  8015  axpre-apti  8095  nntopi  8104  subval  8361  eqord1  8653  divvalap  8844  nn0ind-raph  9587  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  wrdind  11293  wrd2ind  11294  reuccatpfxs1lem  11317  sqrtrval  11551  summodclem2  11933  prodmodclem2  12128  divides  12340  dvdstr  12379  odd2np1lem  12423  ndvdssub  12481  bitsinv1  12513  eucalglt  12619  hashgcdeq  12802  ennnfonelemim  13035  imasaddfnlemg  13387  dfgrp2  13600  grpidinv  13632  dfgrp3mlem  13671  isdomn  14273  xmeteq0  15073  mpodvdsmulf1o  15704  gausslemma2dlem0i  15776  upgredgpr  15988  ushgredgedg  16065  ushgredgedgloop  16067  uspgr2wlkeq  16162  clwwlkng  16200  clwwlkext2edg  16217  clwwlknon  16224  clwwlk0on0  16226  pw1dceq  16541  trilpo  16583  trirec0  16584  redcwlpo  16595  redc0  16597  reap0  16598