Theorem eqeq2 2214

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

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

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqeq2i  2215  eqeq2d  2216  eqeq12  2217  eleq1  2267  neeq2  2389  alexeq  2898  ceqex  2899  pm13.183  2910  eqeu  2942  mo2icl  2951  mob2  2952  euind  2959  reu6i  2963  reuind  2977  sbc5  3021  csbiebg  3135  sneq  3643  preqr1g  3806  preqr1  3808  prel12  3811  preq12bg  3813  opth  4280  euotd  4298  ordtriexmid  4568  ontriexmidim  4569  wetriext  4624  tfisi  4634  ideqg  4828  resieq  4968  cnveqb  5137  cnveq0  5138  iota5  5252  funopg  5304  fneq2  5362  foeq3  5495  tz6.12f  5604  funbrfv  5616  fnbrfvb  5618  fvelimab  5634  elrnrexdm  5718  eufnfv  5814  f1veqaeq  5837  mpoeq123  6003  ovmpt4g  6067  ovi3  6082  ovg  6084  caovcang  6107  caovcan  6110  uchoice  6222  frecabcl  6484  nntri3or  6578  dcdifsnid  6589  nnaordex  6613  nnawordex  6614  ereq2  6627  eroveu  6712  2dom  6896  fundmen  6897  xpf1o  6940  nneneq  6953  tridc  6995  prfidceq  7024  tpfidceq  7026  fisseneq  7030  fidcenumlemrks  7054  supsnti  7106  isotilem  7107  updjud  7183  nninfwlpoimlemdc  7278  exmidontriimlem3  7334  exmidontriimlem4  7335  onntri35  7348  exmidapne  7371  nqtri3or  7508  ltexnqq  7520  aptisr  7891  srpospr  7895  map2psrprg  7917  axpre-apti  7997  nntopi  8006  subval  8263  eqord1  8555  divvalap  8746  nn0ind-raph  9489  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  sqrtrval  11253  summodclem2  11635  prodmodclem2  11830  divides  12042  dvdstr  12081  odd2np1lem  12125  ndvdssub  12183  bitsinv1  12215  eucalglt  12321  hashgcdeq  12504  ennnfonelemim  12737  imasaddfnlemg  13088  dfgrp2  13301  grpidinv  13333  dfgrp3mlem  13372  isdomn  13973  xmeteq0  14773  mpodvdsmulf1o  15404  gausslemma2dlem0i  15476  trilpo  15915  trirec0  15916  redcwlpo  15927  redc0  15929  reap0  15930