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  5884  f1veqaeq  5909  mpoeq123  6079  ovmpt4g  6143  ovi3  6158  ovg  6160  caovcang  6183  caovcan  6186  uchoice  6299  frecabcl  6564  nntri3or  6660  dcdifsnid  6671  nnaordex  6695  nnawordex  6696  ereq2  6709  eroveu  6794  2dom  6979  fundmen  6980  xpf1o  7029  nneneq  7042  tridc  7088  elssdc  7093  eqsndc  7094  prfidceq  7119  tpfidceq  7121  fisseneq  7126  fidcenumlemrks  7151  supsnti  7203  isotilem  7204  updjud  7280  nninfwlpoimlemdc  7375  exmidontriimlem3  7437  exmidontriimlem4  7438  onntri35  7454  exmidapne  7478  nqtri3or  7615  ltexnqq  7627  aptisr  7998  srpospr  8002  map2psrprg  8024  axpre-apti  8104  nntopi  8113  subval  8370  eqord1  8662  divvalap  8853  nn0ind-raph  9596  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  wrdind  11302  wrd2ind  11303  reuccatpfxs1lem  11326  sqrtrval  11560  summodclem2  11942  prodmodclem2  12137  divides  12349  dvdstr  12388  odd2np1lem  12432  ndvdssub  12490  bitsinv1  12522  eucalglt  12628  hashgcdeq  12811  ennnfonelemim  13044  imasaddfnlemg  13396  dfgrp2  13609  grpidinv  13641  dfgrp3mlem  13680  isdomn  14282  xmeteq0  15082  mpodvdsmulf1o  15713  gausslemma2dlem0i  15785  upgredgpr  15999  ushgredgedg  16076  ushgredgedgloop  16078  uspgr2wlkeq  16215  clwwlkng  16255  clwwlkext2edg  16272  clwwlknon  16279  clwwlk0on0  16281  pw1dceq  16605  trilpo  16647  trirec0  16648  redcwlpo  16659  redc0  16661  reap0  16662