Theorem eqeq2 2094

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078

This theorem is referenced by:  eqeq2i  2095  eqeq2d  2096  eqeq12  2097  eleq1  2147  neeq2  2265  alexeq  2734  ceqex  2735  pm13.183  2745  eqeu  2776  mo2icl  2785  mob2  2786  euind  2793  reu6i  2797  reuind  2809  sbc5  2852  csbiebg  2959  sneq  3442  preqr1g  3593  preqr1  3595  prel12  3598  preq12bg  3600  opth  4037  euotd  4054  ordtriexmid  4310  wetriext  4364  tfisi  4374  ideqg  4554  resieq  4690  cnveqb  4849  cnveq0  4850  iota5  4963  funopg  5010  fneq2  5065  foeq3  5188  tz6.12f  5290  funbrfv  5300  fnbrfvb  5302  fvelimab  5317  elrnrexdm  5395  eufnfv  5480  f1veqaeq  5503  mpt2eq123  5659  ovmpt4g  5718  ovi3  5732  ovg  5734  caovcang  5757  caovcan  5760  frecabcl  6112  nntri3or  6202  dcdifsnid  6211  nnaordex  6232  nnawordex  6233  ereq2  6246  eroveu  6329  2dom  6468  fundmen  6469  xpf1o  6506  nneneq  6519  tridc  6561  fisseneq  6586  supsnti  6637  isotilem  6638  updjud  6710  nqtri3or  6892  ltexnqq  6904  aptisr  7261  srpospr  7265  axpre-apti  7357  nntopi  7366  subval  7611  divvalap  8073  nn0ind-raph  8789  frecuzrdgtcl  9740  frecuzrdgfunlem  9747  sqrtrval  10321  isummolem2  10654  divides  10665  dvdstr  10700  odd2np1lem  10739  ndvdssub  10797  eucalglt  10906  hashgcdeq  11071