Theorem eqeq2 2180

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqeq2i  2181  eqeq2d  2182  eqeq12  2183  eleq1  2233  neeq2  2354  alexeq  2856  ceqex  2857  pm13.183  2868  eqeu  2900  mo2icl  2909  mob2  2910  euind  2917  reu6i  2921  reuind  2935  sbc5  2978  csbiebg  3091  sneq  3592  preqr1g  3751  preqr1  3753  prel12  3756  preq12bg  3758  opth  4220  euotd  4237  ordtriexmid  4503  ontriexmidim  4504  wetriext  4559  tfisi  4569  ideqg  4760  resieq  4899  cnveqb  5064  cnveq0  5065  iota5  5178  funopg  5230  fneq2  5285  foeq3  5416  tz6.12f  5523  funbrfv  5533  fnbrfvb  5535  fvelimab  5550  elrnrexdm  5632  eufnfv  5723  f1veqaeq  5745  mpoeq123  5909  ovmpt4g  5972  ovi3  5986  ovg  5988  caovcang  6011  caovcan  6014  frecabcl  6375  nntri3or  6469  dcdifsnid  6480  nnaordex  6503  nnawordex  6504  ereq2  6517  eroveu  6600  2dom  6779  fundmen  6780  xpf1o  6818  nneneq  6831  tridc  6873  fisseneq  6905  fidcenumlemrks  6926  supsnti  6978  isotilem  6979  updjud  7055  exmidontriimlem3  7187  exmidontriimlem4  7188  onntri35  7201  nqtri3or  7345  ltexnqq  7357  aptisr  7728  srpospr  7732  map2psrprg  7754  axpre-apti  7834  nntopi  7843  subval  8098  eqord1  8389  divvalap  8578  nn0ind-raph  9316  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  sqrtrval  10951  summodclem2  11332  prodmodclem2  11527  divides  11738  dvdstr  11777  odd2np1lem  11818  ndvdssub  11876  eucalglt  11998  hashgcdeq  12180  ennnfonelemim  12366  xmeteq0  13074  trilpo  13997  trirec0  13998  redcwlpo  14009  redc0  14011  reap0  14012