Theorem eqeq2 2239

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeq2i  2240  eqeq2d  2241  eqeq12  2242  eleq1  2292  neeq2  2414  alexeq  2929  ceqex  2930  pm13.183  2941  eqeu  2973  mo2icl  2982  mob2  2983  euind  2990  reu6i  2994  reuind  3008  sbc5  3052  csbiebg  3167  sneq  3677  preqr1g  3844  preqr1  3846  prel12  3849  preq12bg  3851  opth  4323  euotd  4341  ordtriexmid  4613  ontriexmidim  4614  wetriext  4669  tfisi  4679  ideqg  4873  resieq  5015  cnveqb  5184  cnveq0  5185  iota5  5300  funopg  5352  fneq2  5410  foeq3  5548  tz6.12f  5658  funbrfv  5672  fnbrfvb  5674  fvelimab  5692  elrnrexdm  5776  eufnfv  5874  f1veqaeq  5899  mpoeq123  6069  ovmpt4g  6133  ovi3  6148  ovg  6150  caovcang  6173  caovcan  6176  uchoice  6289  frecabcl  6551  nntri3or  6647  dcdifsnid  6658  nnaordex  6682  nnawordex  6683  ereq2  6696  eroveu  6781  2dom  6966  fundmen  6967  xpf1o  7013  nneneq  7026  tridc  7070  elssdc  7075  eqsndc  7076  prfidceq  7101  tpfidceq  7103  fisseneq  7107  fidcenumlemrks  7131  supsnti  7183  isotilem  7184  updjud  7260  nninfwlpoimlemdc  7355  exmidontriimlem3  7416  exmidontriimlem4  7417  onntri35  7433  exmidapne  7457  nqtri3or  7594  ltexnqq  7606  aptisr  7977  srpospr  7981  map2psrprg  8003  axpre-apti  8083  nntopi  8092  subval  8349  eqord1  8641  divvalap  8832  nn0ind-raph  9575  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  wrdind  11269  wrd2ind  11270  reuccatpfxs1lem  11293  sqrtrval  11526  summodclem2  11908  prodmodclem2  12103  divides  12315  dvdstr  12354  odd2np1lem  12398  ndvdssub  12456  bitsinv1  12488  eucalglt  12594  hashgcdeq  12777  ennnfonelemim  13010  imasaddfnlemg  13362  dfgrp2  13575  grpidinv  13607  dfgrp3mlem  13646  isdomn  14248  xmeteq0  15048  mpodvdsmulf1o  15679  gausslemma2dlem0i  15751  upgredgpr  15962  ushgredgedg  16039  ushgredgedgloop  16041  uspgr2wlkeq  16106  pw1dceq  16429  trilpo  16471  trirec0  16472  redcwlpo  16483  redc0  16485  reap0  16486