Theorem eqeq2 2175

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqeq2i  2176  eqeq2d  2177  eqeq12  2178  eleq1  2229  neeq2  2350  alexeq  2852  ceqex  2853  pm13.183  2864  eqeu  2896  mo2icl  2905  mob2  2906  euind  2913  reu6i  2917  reuind  2931  sbc5  2974  csbiebg  3087  sneq  3587  preqr1g  3746  preqr1  3748  prel12  3751  preq12bg  3753  opth  4215  euotd  4232  ordtriexmid  4498  ontriexmidim  4499  wetriext  4554  tfisi  4564  ideqg  4755  resieq  4894  cnveqb  5059  cnveq0  5060  iota5  5173  funopg  5222  fneq2  5277  foeq3  5408  tz6.12f  5515  funbrfv  5525  fnbrfvb  5527  fvelimab  5542  elrnrexdm  5624  eufnfv  5715  f1veqaeq  5737  mpoeq123  5901  ovmpt4g  5964  ovi3  5978  ovg  5980  caovcang  6003  caovcan  6006  frecabcl  6367  nntri3or  6461  dcdifsnid  6472  nnaordex  6495  nnawordex  6496  ereq2  6509  eroveu  6592  2dom  6771  fundmen  6772  xpf1o  6810  nneneq  6823  tridc  6865  fisseneq  6897  fidcenumlemrks  6918  supsnti  6970  isotilem  6971  updjud  7047  exmidontriimlem3  7179  exmidontriimlem4  7180  onntri35  7193  nqtri3or  7337  ltexnqq  7349  aptisr  7720  srpospr  7724  map2psrprg  7746  axpre-apti  7826  nntopi  7835  subval  8090  eqord1  8381  divvalap  8570  nn0ind-raph  9308  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  sqrtrval  10942  summodclem2  11323  prodmodclem2  11518  divides  11729  dvdstr  11768  odd2np1lem  11809  ndvdssub  11867  eucalglt  11989  hashgcdeq  12171  ennnfonelemim  12357  xmeteq0  12999  trilpo  13922  trirec0  13923  redcwlpo  13934  redc0  13936  reap0  13937