Theorem eqeq2 2206

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 2203	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2198	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2198	. 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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqeq2i  2207  eqeq2d  2208  eqeq12  2209  eleq1  2259  neeq2  2381  alexeq  2890  ceqex  2891  pm13.183  2902  eqeu  2934  mo2icl  2943  mob2  2944  euind  2951  reu6i  2955  reuind  2969  sbc5  3013  csbiebg  3127  sneq  3634  preqr1g  3797  preqr1  3799  prel12  3802  preq12bg  3804  opth  4271  euotd  4288  ordtriexmid  4558  ontriexmidim  4559  wetriext  4614  tfisi  4624  ideqg  4818  resieq  4957  cnveqb  5126  cnveq0  5127  iota5  5241  funopg  5293  fneq2  5348  foeq3  5481  tz6.12f  5590  funbrfv  5602  fnbrfvb  5604  fvelimab  5620  elrnrexdm  5704  eufnfv  5796  f1veqaeq  5819  mpoeq123  5985  ovmpt4g  6049  ovi3  6064  ovg  6066  caovcang  6089  caovcan  6092  uchoice  6204  frecabcl  6466  nntri3or  6560  dcdifsnid  6571  nnaordex  6595  nnawordex  6596  ereq2  6609  eroveu  6694  2dom  6873  fundmen  6874  xpf1o  6914  nneneq  6927  tridc  6969  prfidceq  6998  tpfidceq  7000  fisseneq  7004  fidcenumlemrks  7028  supsnti  7080  isotilem  7081  updjud  7157  nninfwlpoimlemdc  7252  exmidontriimlem3  7308  exmidontriimlem4  7309  onntri35  7322  exmidapne  7345  nqtri3or  7482  ltexnqq  7494  aptisr  7865  srpospr  7869  map2psrprg  7891  axpre-apti  7971  nntopi  7980  subval  8237  eqord1  8529  divvalap  8720  nn0ind-raph  9462  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  sqrtrval  11184  summodclem2  11566  prodmodclem2  11761  divides  11973  dvdstr  12012  odd2np1lem  12056  ndvdssub  12114  bitsinv1  12146  eucalglt  12252  hashgcdeq  12435  ennnfonelemim  12668  imasaddfnlemg  13018  dfgrp2  13231  grpidinv  13263  dfgrp3mlem  13302  isdomn  13903  xmeteq0  14703  mpodvdsmulf1o  15334  gausslemma2dlem0i  15406  trilpo  15800  trirec0  15801  redcwlpo  15812  redc0  15814  reap0  15815