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  3594  preqr1g  3753  preqr1  3755  prel12  3758  preq12bg  3760  opth  4222  euotd  4239  ordtriexmid  4505  ontriexmidim  4506  wetriext  4561  tfisi  4571  ideqg  4762  resieq  4901  cnveqb  5066  cnveq0  5067  iota5  5180  funopg  5232  fneq2  5287  foeq3  5418  tz6.12f  5525  funbrfv  5535  fnbrfvb  5537  fvelimab  5552  elrnrexdm  5635  eufnfv  5726  f1veqaeq  5748  mpoeq123  5912  ovmpt4g  5975  ovi3  5989  ovg  5991  caovcang  6014  caovcan  6017  frecabcl  6378  nntri3or  6472  dcdifsnid  6483  nnaordex  6507  nnawordex  6508  ereq2  6521  eroveu  6604  2dom  6783  fundmen  6784  xpf1o  6822  nneneq  6835  tridc  6877  fisseneq  6909  fidcenumlemrks  6930  supsnti  6982  isotilem  6983  updjud  7059  nninfwlpoimlemdc  7153  exmidontriimlem3  7200  exmidontriimlem4  7201  onntri35  7214  nqtri3or  7358  ltexnqq  7370  aptisr  7741  srpospr  7745  map2psrprg  7767  axpre-apti  7847  nntopi  7856  subval  8111  eqord1  8402  divvalap  8591  nn0ind-raph  9329  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  sqrtrval  10964  summodclem2  11345  prodmodclem2  11540  divides  11751  dvdstr  11790  odd2np1lem  11831  ndvdssub  11889  eucalglt  12011  hashgcdeq  12193  ennnfonelemim  12379  dfgrp2  12732  grpidinv  12759  xmeteq0  13153  trilpo  14075  trirec0  14076  redcwlpo  14087  redc0  14089  reap0  14090