Theorem eqeq2 2203

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqeq2i  2204  eqeq2d  2205  eqeq12  2206  eleq1  2256  neeq2  2378  alexeq  2886  ceqex  2887  pm13.183  2898  eqeu  2930  mo2icl  2939  mob2  2940  euind  2947  reu6i  2951  reuind  2965  sbc5  3009  csbiebg  3123  sneq  3629  preqr1g  3792  preqr1  3794  prel12  3797  preq12bg  3799  opth  4266  euotd  4283  ordtriexmid  4553  ontriexmidim  4554  wetriext  4609  tfisi  4619  ideqg  4813  resieq  4952  cnveqb  5121  cnveq0  5122  iota5  5236  funopg  5288  fneq2  5343  foeq3  5474  tz6.12f  5583  funbrfv  5595  fnbrfvb  5597  fvelimab  5613  elrnrexdm  5697  eufnfv  5789  f1veqaeq  5812  mpoeq123  5977  ovmpt4g  6041  ovi3  6055  ovg  6057  caovcang  6080  caovcan  6083  uchoice  6190  frecabcl  6452  nntri3or  6546  dcdifsnid  6557  nnaordex  6581  nnawordex  6582  ereq2  6595  eroveu  6680  2dom  6859  fundmen  6860  xpf1o  6900  nneneq  6913  tridc  6955  fisseneq  6988  fidcenumlemrks  7012  supsnti  7064  isotilem  7065  updjud  7141  nninfwlpoimlemdc  7236  exmidontriimlem3  7283  exmidontriimlem4  7284  onntri35  7297  exmidapne  7320  nqtri3or  7456  ltexnqq  7468  aptisr  7839  srpospr  7843  map2psrprg  7865  axpre-apti  7945  nntopi  7954  subval  8211  eqord1  8502  divvalap  8693  nn0ind-raph  9434  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  sqrtrval  11144  summodclem2  11525  prodmodclem2  11720  divides  11932  dvdstr  11971  odd2np1lem  12013  ndvdssub  12071  eucalglt  12195  hashgcdeq  12377  ennnfonelemim  12581  imasaddfnlemg  12897  dfgrp2  13099  grpidinv  13131  dfgrp3mlem  13170  isdomn  13765  xmeteq0  14527  gausslemma2dlem0i  15173  trilpo  15533  trirec0  15534  redcwlpo  15545  redc0  15547  reap0  15548