Theorem eqeq2 2031

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 2028	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
2		eqcom 2024	. 2 ⊢ (𝐶 = A ↔ A = 𝐶)
3		eqcom 2024	. 2 ⊢ (𝐶 = B ↔ B = 𝐶)
4	1, 2, 3	3bitr4g 212	1 ⊢ (A = B → (𝐶 = A ↔ 𝐶 = B))

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

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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004

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

This theorem is referenced by:  eqeq2i  2032  eqeq2d  2033  eqeq12  2034  eleq1  2082  neeq2  2198  alexeq  2647  ceqex  2648  pm13.183  2658  eqeu  2688  mo2icl  2697  mob2  2698  euind  2705  reu6i  2709  reuind  2721  sbc5  2764  csbiebg  2866  sneq  3361  preqr1g  3511  preqr1  3513  prel12  3516  preq12bg  3518  opth  3948  euotd  3965  ordtriexmid  4194  tfisi  4237  ideqg  4414  resieq  4549  cnveqb  4703  cnveq0  4704  iota5  4814  funopg  4860  fneq2  4914  foeq3  5029  tz6.12f  5127  funbrfv  5137  fnbrfvb  5139  fvelimab  5154  elrnrexdm  5231  eufnfv  5314  f1veqaeq  5333  mpt2eq123  5487  ovmpt4g  5546  ovi3  5560  ovg  5562  caovcang  5585  caovcan  5588  nntri3or  5987  nnaordex  6011  nnawordex  6012  ereq2  6025  eroveu  6108  nqtri3or  6255  ltexnqq  6266  subval  6790