Theorem eqeq2 2049

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

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

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  eqeq2i  2050  eqeq2d  2051  eqeq12  2052  eleq1  2100  neeq2  2219  alexeq  2670  ceqex  2671  pm13.183  2681  eqeu  2711  mo2icl  2720  mob2  2721  euind  2728  reu6i  2732  reuind  2744  sbc5  2787  csbiebg  2889  sneq  3386  preqr1g  3537  preqr1  3539  prel12  3542  preq12bg  3544  opth  3974  euotd  3991  ordtriexmid  4247  wetriext  4301  tfisi  4310  ideqg  4487  resieq  4622  cnveqb  4776  cnveq0  4777  iota5  4887  funopg  4934  fneq2  4988  foeq3  5104  tz6.12f  5202  funbrfv  5212  fnbrfvb  5214  fvelimab  5229  elrnrexdm  5306  eufnfv  5389  f1veqaeq  5408  mpt2eq123  5564  ovmpt4g  5623  ovi3  5637  ovg  5639  caovcang  5662  caovcan  5665  nntri3or  6072  nnaordex  6100  nnawordex  6101  ereq2  6114  eroveu  6197  2dom  6285  fundmen  6286  nneneq  6320  nqtri3or  6494  ltexnqq  6506  aptisr  6863  srpospr  6867  axpre-apti  6959  nntopi  6968  subval  7203  divvalap  7653  nn0ind-raph  8355  frecuzrdgfn  9198  sqrtrval  9598