Theorem eqeq2 2109

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  eqeq2i  2110  eqeq2d  2111  eqeq12  2112  eleq1  2162  neeq2  2281  alexeq  2765  ceqex  2766  pm13.183  2776  eqeu  2807  mo2icl  2816  mob2  2817  euind  2824  reu6i  2828  reuind  2842  sbc5  2885  csbiebg  2992  sneq  3485  preqr1g  3640  preqr1  3642  prel12  3645  preq12bg  3647  opth  4097  euotd  4114  ordtriexmid  4375  wetriext  4429  tfisi  4439  ideqg  4628  resieq  4765  cnveqb  4930  cnveq0  4931  iota5  5044  funopg  5093  fneq2  5148  foeq3  5279  tz6.12f  5382  funbrfv  5392  fnbrfvb  5394  fvelimab  5409  elrnrexdm  5491  eufnfv  5580  f1veqaeq  5602  mpoeq123  5762  ovmpt4g  5825  ovi3  5839  ovg  5841  caovcang  5864  caovcan  5867  frecabcl  6226  nntri3or  6319  dcdifsnid  6330  nnaordex  6353  nnawordex  6354  ereq2  6367  eroveu  6450  2dom  6629  fundmen  6630  xpf1o  6667  nneneq  6680  tridc  6722  fisseneq  6749  fidcenumlemrks  6769  supsnti  6807  isotilem  6808  updjud  6882  nqtri3or  7105  ltexnqq  7117  aptisr  7474  srpospr  7478  axpre-apti  7570  nntopi  7579  subval  7825  eqord1  8112  divvalap  8295  nn0ind-raph  9020  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  sqrtrval  10612  summodclem2  10990  divides  11290  dvdstr  11325  odd2np1lem  11364  ndvdssub  11422  eucalglt  11531  hashgcdeq  11696  ennnfonelemim  11729  xmeteq0  12287  trilpo  12820