Theorem eqeq2 2149

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  eqeq2i  2150  eqeq2d  2151  eqeq12  2152  eleq1  2202  neeq2  2322  alexeq  2811  ceqex  2812  pm13.183  2822  eqeu  2854  mo2icl  2863  mob2  2864  euind  2871  reu6i  2875  reuind  2889  sbc5  2932  csbiebg  3042  sneq  3538  preqr1g  3693  preqr1  3695  prel12  3698  preq12bg  3700  opth  4159  euotd  4176  ordtriexmid  4437  wetriext  4491  tfisi  4501  ideqg  4690  resieq  4829  cnveqb  4994  cnveq0  4995  iota5  5108  funopg  5157  fneq2  5212  foeq3  5343  tz6.12f  5450  funbrfv  5460  fnbrfvb  5462  fvelimab  5477  elrnrexdm  5559  eufnfv  5648  f1veqaeq  5670  mpoeq123  5830  ovmpt4g  5893  ovi3  5907  ovg  5909  caovcang  5932  caovcan  5935  frecabcl  6296  nntri3or  6389  dcdifsnid  6400  nnaordex  6423  nnawordex  6424  ereq2  6437  eroveu  6520  2dom  6699  fundmen  6700  xpf1o  6738  nneneq  6751  tridc  6793  fisseneq  6820  fidcenumlemrks  6841  supsnti  6892  isotilem  6893  updjud  6967  nqtri3or  7204  ltexnqq  7216  aptisr  7587  srpospr  7591  map2psrprg  7613  axpre-apti  7693  nntopi  7702  subval  7954  eqord1  8245  divvalap  8434  nn0ind-raph  9168  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  sqrtrval  10772  summodclem2  11151  prodmodclem2  11346  divides  11495  dvdstr  11530  odd2np1lem  11569  ndvdssub  11627  eucalglt  11738  hashgcdeq  11904  ennnfonelemim  11937  xmeteq0  12528  trilpo  13236