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  3843  preqr1  3845  prel12  3848  preq12bg  3850  opth  4322  euotd  4340  ordtriexmid  4612  ontriexmidim  4613  wetriext  4668  tfisi  4678  ideqg  4872  resieq  5014  cnveqb  5183  cnveq0  5184  iota5  5299  funopg  5351  fneq2  5409  foeq3  5545  tz6.12f  5655  funbrfv  5669  fnbrfvb  5671  fvelimab  5689  elrnrexdm  5773  eufnfv  5869  f1veqaeq  5892  mpoeq123  6062  ovmpt4g  6126  ovi3  6141  ovg  6143  caovcang  6166  caovcan  6169  uchoice  6281  frecabcl  6543  nntri3or  6637  dcdifsnid  6648  nnaordex  6672  nnawordex  6673  ereq2  6686  eroveu  6771  2dom  6956  fundmen  6957  xpf1o  7001  nneneq  7014  tridc  7057  prfidceq  7086  tpfidceq  7088  fisseneq  7092  fidcenumlemrks  7116  supsnti  7168  isotilem  7169  updjud  7245  nninfwlpoimlemdc  7340  exmidontriimlem3  7401  exmidontriimlem4  7402  onntri35  7418  exmidapne  7442  nqtri3or  7579  ltexnqq  7591  aptisr  7962  srpospr  7966  map2psrprg  7988  axpre-apti  8068  nntopi  8077  subval  8334  eqord1  8626  divvalap  8817  nn0ind-raph  9560  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  wrdind  11249  wrd2ind  11250  reuccatpfxs1lem  11273  sqrtrval  11506  summodclem2  11888  prodmodclem2  12083  divides  12295  dvdstr  12334  odd2np1lem  12378  ndvdssub  12436  bitsinv1  12468  eucalglt  12574  hashgcdeq  12757  ennnfonelemim  12990  imasaddfnlemg  13342  dfgrp2  13555  grpidinv  13587  dfgrp3mlem  13626  isdomn  14227  xmeteq0  15027  mpodvdsmulf1o  15658  gausslemma2dlem0i  15730  upgredgpr  15941  ushgredgedg  16018  ushgredgedgloop  16020  trilpo  16370  trirec0  16371  redcwlpo  16382  redc0  16384  reap0  16385