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  7346  isotilem  7347  updjud  7423  nninfwlpoimlemdc  7518  exmidontriimlem3  7580  exmidontriimlem4  7581  onntri35  7597  exmidapne  7627  nqtri3or  7764  ltexnqq  7776  aptisr  8147  srpospr  8151  map2psrprg  8173  axpre-apti  8253  nntopi  8262  subval  8520  eqord1  8813  divvalap  9007  nn0ind-raph  9768  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  hashfibclem  11298  hashfibc  11299  wrdind  11510  wrd2ind  11511  reuccatpfxs1lem  11534  sqrtrval  11782  summodclem2  12168  prodmodclem2  12363  divides  12575  dvdstr  12614  odd2np1lem  12658  ndvdssub  12716  bitsinv1  12748  eucalglt  12854  hashgcdeq  13041  ennnfonelemim  13367  imasaddfnlemg  13688  dfgrp2  13885  grpidinv  13917  dfgrp3mlem  13956  isdomn  14662  xmeteq0  15551  mpodvdsmulf1o  16245  gausslemma2dlem0i  16342  upgredgpr  16556  ushgredgedg  16633  ushgredgedgloop  16635  uspgr2wlkeq  16772  clwwlkng  16812  clwwlkext2edg  16829  clwwlknon  16836  clwwlk0on0  16838  pw1dceq  17201  trilpo  17259  trirec0  17260  redcwlpo  17272  redc0  17274  reap0  17275