Theorem eqeq2 2199

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  eqeq2i  2200  eqeq2d  2201  eqeq12  2202  eleq1  2252  neeq2  2374  alexeq  2878  ceqex  2879  pm13.183  2890  eqeu  2922  mo2icl  2931  mob2  2932  euind  2939  reu6i  2943  reuind  2957  sbc5  3001  csbiebg  3114  sneq  3618  preqr1g  3781  preqr1  3783  prel12  3786  preq12bg  3788  opth  4252  euotd  4269  ordtriexmid  4535  ontriexmidim  4536  wetriext  4591  tfisi  4601  ideqg  4793  resieq  4932  cnveqb  5099  cnveq0  5100  iota5  5214  funopg  5266  fneq2  5321  foeq3  5452  tz6.12f  5560  funbrfv  5571  fnbrfvb  5573  fvelimab  5589  elrnrexdm  5672  eufnfv  5764  f1veqaeq  5787  mpoeq123  5951  ovmpt4g  6015  ovi3  6029  ovg  6031  caovcang  6054  caovcan  6057  frecabcl  6419  nntri3or  6513  dcdifsnid  6524  nnaordex  6548  nnawordex  6549  ereq2  6562  eroveu  6647  2dom  6826  fundmen  6827  xpf1o  6867  nneneq  6880  tridc  6922  fisseneq  6955  fidcenumlemrks  6977  supsnti  7029  isotilem  7030  updjud  7106  nninfwlpoimlemdc  7200  exmidontriimlem3  7247  exmidontriimlem4  7248  onntri35  7261  exmidapne  7284  nqtri3or  7420  ltexnqq  7432  aptisr  7803  srpospr  7807  map2psrprg  7829  axpre-apti  7909  nntopi  7918  subval  8174  eqord1  8465  divvalap  8656  nn0ind-raph  9395  frecuzrdgtcl  10438  frecuzrdgfunlem  10445  sqrtrval  11036  summodclem2  11417  prodmodclem2  11612  divides  11823  dvdstr  11862  odd2np1lem  11904  ndvdssub  11962  eucalglt  12084  hashgcdeq  12266  ennnfonelemim  12470  imasaddfnlemg  12784  dfgrp2  12964  grpidinv  12996  dfgrp3mlem  13035  xmeteq0  14296  trilpo  15229  trirec0  15230  redcwlpo  15241  redc0  15243  reap0  15244