Theorem eqeq2 2242

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 2239	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqcom 2234	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶)
3		eqcom 2234	. 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 2214

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

This theorem is referenced by:  eqeq2i  2243  eqeq2d  2244  eqeq12  2245  eleq1  2295  neeq2  2426  alexeq  2943  ceqex  2944  pm13.183  2955  eqeu  2987  mo2icl  2996  mob2  2997  euind  3004  reu6i  3008  reuind  3022  sbc5  3066  csbiebg  3181  sneq  3700  preqr1g  3870  preqr1  3872  prel12  3875  preq12bg  3877  opth  4353  euotd  4371  ordtriexmid  4643  ontriexmidim  4644  wetriext  4699  tfisi  4709  ideqg  4906  resieq  5048  cnveqb  5218  cnveq0  5219  iota5  5334  funopg  5386  fneq2  5445  foeq3  5588  tz6.12f  5699  funbrfv  5713  fnbrfvb  5715  fvelimab  5733  elrnrexdm  5816  eufnfv  5917  f1veqaeq  5942  mpoeq123  6112  ovmpt4g  6176  ovi3  6191  ovg  6193  caovcang  6216  caovcan  6219  uchoice  6331  suppssrst  6461  suppssrgst  6462  frecabcl  6630  nntri3or  6726  dcdifsnid  6737  nnaordex  6761  nnawordex  6762  ereq2  6775  eroveu  6860  2dom  7046  fundmen  7047  xpf1o  7097  nneneq  7111  tridc  7157  elssdc  7162  eqsndc  7163  prfidceq  7188  tpfidceq  7190  fisseneq  7195  fidcenumlemrks  7223  supsnti  7296  isotilem  7297  updjud  7373  nninfwlpoimlemdc  7468  exmidontriimlem3  7530  exmidontriimlem4  7531  onntri35  7547  exmidapne  7574  nqtri3or  7711  ltexnqq  7723  aptisr  8094  srpospr  8098  map2psrprg  8120  axpre-apti  8200  nntopi  8209  subval  8465  eqord1  8757  divvalap  8948  nn0ind-raph  9695  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  hashfibclem  11206  hashfibc  11207  wrdind  11414  wrd2ind  11415  reuccatpfxs1lem  11438  sqrtrval  11685  summodclem2  12068  prodmodclem2  12263  divides  12475  dvdstr  12514  odd2np1lem  12558  ndvdssub  12616  bitsinv1  12648  eucalglt  12754  hashgcdeq  12937  ennnfonelemim  13175  imasaddfnlemg  13527  dfgrp2  13740  grpidinv  13772  dfgrp3mlem  13811  isdomn  14415  xmeteq0  15224  mpodvdsmulf1o  15858  gausslemma2dlem0i  15930  upgredgpr  16144  ushgredgedg  16221  ushgredgedgloop  16223  uspgr2wlkeq  16360  clwwlkng  16400  clwwlkext2edg  16417  clwwlknon  16424  clwwlk0on0  16426  pw1dceq  16778  trilpo  16827  trirec0  16828  redcwlpo  16840  redc0  16842  reap0  16843