Theorem eqeq2 2216

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqeq2i  2217  eqeq2d  2218  eqeq12  2219  eleq1  2269  neeq2  2391  alexeq  2903  ceqex  2904  pm13.183  2915  eqeu  2947  mo2icl  2956  mob2  2957  euind  2964  reu6i  2968  reuind  2982  sbc5  3026  csbiebg  3140  sneq  3649  preqr1g  3813  preqr1  3815  prel12  3818  preq12bg  3820  opth  4289  euotd  4307  ordtriexmid  4577  ontriexmidim  4578  wetriext  4633  tfisi  4643  ideqg  4837  resieq  4978  cnveqb  5147  cnveq0  5148  iota5  5262  funopg  5314  fneq2  5372  foeq3  5508  tz6.12f  5618  funbrfv  5630  fnbrfvb  5632  fvelimab  5648  elrnrexdm  5732  eufnfv  5828  f1veqaeq  5851  mpoeq123  6017  ovmpt4g  6081  ovi3  6096  ovg  6098  caovcang  6121  caovcan  6124  uchoice  6236  frecabcl  6498  nntri3or  6592  dcdifsnid  6603  nnaordex  6627  nnawordex  6628  ereq2  6641  eroveu  6726  2dom  6911  fundmen  6912  xpf1o  6956  nneneq  6969  tridc  7011  prfidceq  7040  tpfidceq  7042  fisseneq  7046  fidcenumlemrks  7070  supsnti  7122  isotilem  7123  updjud  7199  nninfwlpoimlemdc  7294  exmidontriimlem3  7351  exmidontriimlem4  7352  onntri35  7368  exmidapne  7392  nqtri3or  7529  ltexnqq  7541  aptisr  7912  srpospr  7916  map2psrprg  7938  axpre-apti  8018  nntopi  8027  subval  8284  eqord1  8576  divvalap  8767  nn0ind-raph  9510  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  wrdind  11198  wrd2ind  11199  sqrtrval  11386  summodclem2  11768  prodmodclem2  11963  divides  12175  dvdstr  12214  odd2np1lem  12258  ndvdssub  12316  bitsinv1  12348  eucalglt  12454  hashgcdeq  12637  ennnfonelemim  12870  imasaddfnlemg  13221  dfgrp2  13434  grpidinv  13466  dfgrp3mlem  13505  isdomn  14106  xmeteq0  14906  mpodvdsmulf1o  15537  gausslemma2dlem0i  15609  trilpo  16123  trirec0  16124  redcwlpo  16135  redc0  16137  reap0  16138