Theorem eqeq2 2203

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 2200	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2195	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2195	. 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 2175

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

This theorem is referenced by:  eqeq2i  2204  eqeq2d  2205  eqeq12  2206  eleq1  2256  neeq2  2378  alexeq  2887  ceqex  2888  pm13.183  2899  eqeu  2931  mo2icl  2940  mob2  2941  euind  2948  reu6i  2952  reuind  2966  sbc5  3010  csbiebg  3124  sneq  3630  preqr1g  3793  preqr1  3795  prel12  3798  preq12bg  3800  opth  4267  euotd  4284  ordtriexmid  4554  ontriexmidim  4555  wetriext  4610  tfisi  4620  ideqg  4814  resieq  4953  cnveqb  5122  cnveq0  5123  iota5  5237  funopg  5289  fneq2  5344  foeq3  5475  tz6.12f  5584  funbrfv  5596  fnbrfvb  5598  fvelimab  5614  elrnrexdm  5698  eufnfv  5790  f1veqaeq  5813  mpoeq123  5978  ovmpt4g  6042  ovi3  6057  ovg  6059  caovcang  6082  caovcan  6085  uchoice  6192  frecabcl  6454  nntri3or  6548  dcdifsnid  6559  nnaordex  6583  nnawordex  6584  ereq2  6597  eroveu  6682  2dom  6861  fundmen  6862  xpf1o  6902  nneneq  6915  tridc  6957  fisseneq  6990  fidcenumlemrks  7014  supsnti  7066  isotilem  7067  updjud  7143  nninfwlpoimlemdc  7238  exmidontriimlem3  7285  exmidontriimlem4  7286  onntri35  7299  exmidapne  7322  nqtri3or  7458  ltexnqq  7470  aptisr  7841  srpospr  7845  map2psrprg  7867  axpre-apti  7947  nntopi  7956  subval  8213  eqord1  8504  divvalap  8695  nn0ind-raph  9437  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  sqrtrval  11147  summodclem2  11528  prodmodclem2  11723  divides  11935  dvdstr  11974  odd2np1lem  12016  ndvdssub  12074  eucalglt  12198  hashgcdeq  12380  ennnfonelemim  12584  imasaddfnlemg  12900  dfgrp2  13102  grpidinv  13134  dfgrp3mlem  13173  isdomn  13768  xmeteq0  14538  gausslemma2dlem0i  15214  trilpo  15603  trirec0  15604  redcwlpo  15615  redc0  15617  reap0  15618