Theorem eqeq2 2248

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqeq2i  2249  eqeq2d  2250  eqeq12  2251  eleq1  2301  neeq2  2434  alexeq  2952  ceqex  2953  pm13.183  2964  eqeu  2996  mo2icl  3005  mob2  3006  euind  3013  reu6i  3017  reuind  3031  sbc5  3075  csbiebg  3190  ifeqeqxdc  3687  sneq  3720  preqr1g  3891  preqr1  3893  prel12  3896  preq12bg  3898  opth  4377  euotd  4395  ordtriexmid  4668  ontriexmidim  4669  wetriext  4724  tfisi  4734  ideqg  4931  resieq  5073  cnveqb  5243  cnveq0  5244  iota5  5359  funopg  5411  fneq2  5470  foeq3  5613  tz6.12f  5724  funbrfv  5739  fnbrfvb  5741  fvelimab  5759  elrnrexdm  5847  eufnfv  5949  f1veqaeq  5975  mpoeq123  6147  ovmpt4g  6211  ovi3  6226  ovg  6228  caovcang  6251  caovcan  6254  uchoice  6371  suppssrst  6501  suppssrgst  6502  frecabcl  6670  nntri3or  6766  dcdifsnid  6777  nnaordex  6801  nnawordex  6802  ereq2  6815  eroveu  6900  2dom  7093  fundmen  7094  xpf1o  7144  nneneq  7158  tridc  7204  elssdc  7209  eqsndc  7210  prfidceq  7235  tpfidceq  7237  fisseneq  7242  fidcenumlemrks  7270  supsnti  7345  isotilem  7346  updjud  7422  nninfwlpoimlemdc  7517  exmidontriimlem3  7579  exmidontriimlem4  7580  onntri35  7596  exmidapne  7626  nqtri3or  7763  ltexnqq  7775  aptisr  8146  srpospr  8150  map2psrprg  8172  axpre-apti  8252  nntopi  8261  subval  8518  eqord1  8811  divvalap  9004  nn0ind-raph  9763  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  hashfibclem  11282  hashfibc  11283  wrdind  11494  wrd2ind  11495  reuccatpfxs1lem  11518  sqrtrval  11766  summodclem2  12149  prodmodclem2  12344  divides  12556  dvdstr  12595  odd2np1lem  12639  ndvdssub  12697  bitsinv1  12729  eucalglt  12835  hashgcdeq  13018  ennnfonelemim  13315  imasaddfnlemg  13635  dfgrp2  13832  grpidinv  13864  dfgrp3mlem  13903  isdomn  14578  xmeteq0  15460  mpodvdsmulf1o  16104  gausslemma2dlem0i  16176  upgredgpr  16390  ushgredgedg  16467  ushgredgedgloop  16469  uspgr2wlkeq  16606  clwwlkng  16646  clwwlkext2edg  16663  clwwlknon  16670  clwwlk0on0  16672  pw1dceq  17035  trilpo  17092  trirec0  17093  redcwlpo  17105  redc0  17107  reap0  17108