Theorem eqeq2 2244

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 2241	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2236	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2236	. 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 2216

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

This theorem is referenced by:  eqeq2i  2245  eqeq2d  2246  eqeq12  2247  eleq1  2297  neeq2  2428  alexeq  2946  ceqex  2947  pm13.183  2958  eqeu  2990  mo2icl  2999  mob2  3000  euind  3007  reu6i  3011  reuind  3025  sbc5  3069  csbiebg  3184  ifeqeqxdc  3673  sneq  3705  preqr1g  3875  preqr1  3877  prel12  3880  preq12bg  3882  opth  4358  euotd  4376  ordtriexmid  4648  ontriexmidim  4649  wetriext  4704  tfisi  4714  ideqg  4911  resieq  5053  cnveqb  5223  cnveq0  5224  iota5  5339  funopg  5391  fneq2  5450  foeq3  5593  tz6.12f  5704  funbrfv  5718  fnbrfvb  5720  fvelimab  5738  elrnrexdm  5821  eufnfv  5922  f1veqaeq  5948  mpoeq123  6120  ovmpt4g  6184  ovi3  6199  ovg  6201  caovcang  6224  caovcan  6227  uchoice  6344  suppssrst  6474  suppssrgst  6475  frecabcl  6643  nntri3or  6739  dcdifsnid  6750  nnaordex  6774  nnawordex  6775  ereq2  6788  eroveu  6873  2dom  7059  fundmen  7060  xpf1o  7110  nneneq  7124  tridc  7170  elssdc  7175  eqsndc  7176  prfidceq  7201  tpfidceq  7203  fisseneq  7208  fidcenumlemrks  7236  supsnti  7309  isotilem  7310  updjud  7386  nninfwlpoimlemdc  7481  exmidontriimlem3  7543  exmidontriimlem4  7544  onntri35  7560  exmidapne  7590  nqtri3or  7727  ltexnqq  7739  aptisr  8110  srpospr  8114  map2psrprg  8136  axpre-apti  8216  nntopi  8225  subval  8481  eqord1  8774  divvalap  8965  nn0ind-raph  9713  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  hashfibclem  11231  hashfibc  11232  wrdind  11439  wrd2ind  11440  reuccatpfxs1lem  11463  sqrtrval  11710  summodclem2  12093  prodmodclem2  12288  divides  12500  dvdstr  12539  odd2np1lem  12583  ndvdssub  12641  bitsinv1  12673  eucalglt  12779  hashgcdeq  12962  ennnfonelemim  13259  imasaddfnlemg  13578  dfgrp2  13782  grpidinv  13814  dfgrp3mlem  13853  isdomn  14516  xmeteq0  15350  mpodvdsmulf1o  15984  gausslemma2dlem0i  16056  upgredgpr  16270  ushgredgedg  16347  ushgredgedgloop  16349  uspgr2wlkeq  16486  clwwlkng  16526  clwwlkext2edg  16543  clwwlknon  16550  clwwlk0on0  16552  pw1dceq  16904  trilpo  16953  trirec0  16954  redcwlpo  16966  redc0  16968  reap0  16969