Theorem eqeq2 2046

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq2	⊢ (A = B → (𝐶 = A ↔ 𝐶 = B))

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 2043	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
2		eqcom 2039	. 2 ⊢ (𝐶 = A ↔ A = 𝐶)
3		eqcom 2039	. 2 ⊢ (𝐶 = B ↔ B = 𝐶)
4	1, 2, 3	3bitr4g 212	1 ⊢ (A = B → (𝐶 = A ↔ 𝐶 = B))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqeq2i  2047  eqeq2d  2048  eqeq12  2049  eleq1  2097  neeq2  2214  alexeq  2664  ceqex  2665  pm13.183  2675  eqeu  2705  mo2icl  2714  mob2  2715  euind  2722  reu6i  2726  reuind  2738  sbc5  2781  csbiebg  2883  sneq  3378  preqr1g  3528  preqr1  3530  prel12  3533  preq12bg  3535  opth  3965  euotd  3982  ordtriexmid  4210  tfisi  4253  ideqg  4430  resieq  4565  cnveqb  4719  cnveq0  4720  iota5  4830  funopg  4877  fneq2  4931  foeq3  5047  tz6.12f  5145  funbrfv  5155  fnbrfvb  5157  fvelimab  5172  elrnrexdm  5249  eufnfv  5332  f1veqaeq  5351  mpt2eq123  5506  ovmpt4g  5565  ovi3  5579  ovg  5581  caovcang  5604  caovcan  5607  nntri3or  6011  nnaordex  6036  nnawordex  6037  ereq2  6050  eroveu  6133  2dom  6221  fundmen  6222  nqtri3or  6380  ltexnqq  6391  aptisr  6705  axpre-apti  6769  subval  7000  divvalap  7435  nn0ind-raph  8131  frecuzrdgfn  8879  sqrtrval  9209