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  3377  preqr1g  3527  preqr1  3529  prel12  3532  preq12bg  3534  opth  3964  euotd  3981  ordtriexmid  4209  tfisi  4252  ideqg  4429  resieq  4564  cnveqb  4718  cnveq0  4719  iota5  4829  funopg  4875  fneq2  4929  foeq3  5045  tz6.12f  5143  funbrfv  5153  fnbrfvb  5155  fvelimab  5170  elrnrexdm  5247  eufnfv  5330  f1veqaeq  5349  mpt2eq123  5503  ovmpt4g  5562  ovi3  5576  ovg  5578  caovcang  5601  caovcan  5604  nntri3or  6004  nnaordex  6029  nnawordex  6030  ereq2  6043  eroveu  6126  2dom  6214  fundmen  6215  nqtri3or  6373  ltexnqq  6384  aptisr  6657  axpre-apti  6721  subval  6952  divvalap  7387  nn0ind-raph  8080