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 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced 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  3684  sneq  3716  preqr1g  3886  preqr1  3888  prel12  3891  preq12bg  3893  opth  4372  euotd  4390  ordtriexmid  4663  ontriexmidim  4664  wetriext  4719  tfisi  4729  ideqg  4926  resieq  5068  cnveqb  5238  cnveq0  5239  iota5  5354  funopg  5406  fneq2  5465  foeq3  5608  tz6.12f  5719  funbrfv  5733  fnbrfvb  5735  fvelimab  5753  elrnrexdm  5838  eufnfv  5939  f1veqaeq  5965  mpoeq123  6137  ovmpt4g  6201  ovi3  6216  ovg  6218  caovcang  6241  caovcan  6244  uchoice  6361  suppssrst  6491  suppssrgst  6492  frecabcl  6660  nntri3or  6756  dcdifsnid  6767  nnaordex  6791  nnawordex  6792  ereq2  6805  eroveu  6890  2dom  7083  fundmen  7084  xpf1o  7134  nneneq  7148  tridc  7194  elssdc  7199  eqsndc  7200  prfidceq  7225  tpfidceq  7227  fisseneq  7232  fidcenumlemrks  7260  supsnti  7335  isotilem  7336  updjud  7412  nninfwlpoimlemdc  7507  exmidontriimlem3  7569  exmidontriimlem4  7570  onntri35  7586  exmidapne  7616  nqtri3or  7753  ltexnqq  7765  aptisr  8136  srpospr  8140  map2psrprg  8162  axpre-apti  8242  nntopi  8251  subval  8508  eqord1  8801  divvalap  8994  nn0ind-raph  9742  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  hashfibclem  11260  hashfibc  11261  wrdind  11472  wrd2ind  11473  reuccatpfxs1lem  11496  sqrtrval  11744  summodclem2  12127  prodmodclem2  12322  divides  12534  dvdstr  12573  odd2np1lem  12617  ndvdssub  12675  bitsinv1  12707  eucalglt  12813  hashgcdeq  12996  ennnfonelemim  13293  imasaddfnlemg  13612  dfgrp2  13809  grpidinv  13841  dfgrp3mlem  13880  isdomn  14551  xmeteq0  15383  mpodvdsmulf1o  16018  gausslemma2dlem0i  16090  upgredgpr  16304  ushgredgedg  16381  ushgredgedgloop  16383  uspgr2wlkeq  16520  clwwlkng  16560  clwwlkext2edg  16577  clwwlknon  16584  clwwlk0on0  16586  pw1dceq  16948  trilpo  16997  trirec0  16998  redcwlpo  17010  redc0  17012  reap0  17013