Theorem eqeq2 2241

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqeq2i  2242  eqeq2d  2243  eqeq12  2244  eleq1  2294  neeq2  2417  alexeq  2933  ceqex  2934  pm13.183  2945  eqeu  2977  mo2icl  2986  mob2  2987  euind  2994  reu6i  2998  reuind  3012  sbc5  3056  csbiebg  3171  sneq  3684  preqr1g  3854  preqr1  3856  prel12  3859  preq12bg  3861  opth  4335  euotd  4353  ordtriexmid  4625  ontriexmidim  4626  wetriext  4681  tfisi  4691  ideqg  4887  resieq  5029  cnveqb  5199  cnveq0  5200  iota5  5315  funopg  5367  fneq2  5426  foeq3  5566  tz6.12f  5677  funbrfv  5691  fnbrfvb  5693  fvelimab  5711  elrnrexdm  5794  eufnfv  5895  f1veqaeq  5920  mpoeq123  6090  ovmpt4g  6154  ovi3  6169  ovg  6171  caovcang  6194  caovcan  6197  uchoice  6309  suppssrst  6439  suppssrgst  6440  frecabcl  6608  nntri3or  6704  dcdifsnid  6715  nnaordex  6739  nnawordex  6740  ereq2  6753  eroveu  6838  2dom  7023  fundmen  7024  xpf1o  7073  nneneq  7086  tridc  7132  elssdc  7137  eqsndc  7138  prfidceq  7163  tpfidceq  7165  fisseneq  7170  fidcenumlemrks  7195  supsnti  7247  isotilem  7248  updjud  7324  nninfwlpoimlemdc  7419  exmidontriimlem3  7481  exmidontriimlem4  7482  onntri35  7498  exmidapne  7522  nqtri3or  7659  ltexnqq  7671  aptisr  8042  srpospr  8046  map2psrprg  8068  axpre-apti  8148  nntopi  8157  subval  8413  eqord1  8705  divvalap  8896  nn0ind-raph  9641  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  wrdind  11352  wrd2ind  11353  reuccatpfxs1lem  11376  sqrtrval  11623  summodclem2  12006  prodmodclem2  12201  divides  12413  dvdstr  12452  odd2np1lem  12496  ndvdssub  12554  bitsinv1  12586  eucalglt  12692  hashgcdeq  12875  ennnfonelemim  13108  imasaddfnlemg  13460  dfgrp2  13673  grpidinv  13705  dfgrp3mlem  13744  isdomn  14348  xmeteq0  15153  mpodvdsmulf1o  15787  gausslemma2dlem0i  15859  upgredgpr  16073  ushgredgedg  16150  ushgredgedgloop  16152  uspgr2wlkeq  16289  clwwlkng  16329  clwwlkext2edg  16346  clwwlknon  16353  clwwlk0on0  16355  pw1dceq  16709  trilpo  16758  trirec0  16759  redcwlpo  16771  redc0  16773  reap0  16774