Theorem eqeq2 2092

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

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

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065

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

This theorem is referenced by:  eqeq2i  2093  eqeq2d  2094  eqeq12  2095  eleq1  2145  neeq2  2263  alexeq  2731  ceqex  2732  pm13.183  2742  eqeu  2773  mo2icl  2782  mob2  2783  euind  2790  reu6i  2794  reuind  2806  sbc5  2849  csbiebg  2956  sneq  3433  preqr1g  3584  preqr1  3586  prel12  3589  preq12bg  3591  opth  4028  euotd  4045  ordtriexmid  4301  wetriext  4355  tfisi  4365  ideqg  4545  resieq  4681  cnveqb  4840  cnveq0  4841  iota5  4954  funopg  5001  fneq2  5056  foeq3  5179  tz6.12f  5278  funbrfv  5288  fnbrfvb  5290  fvelimab  5305  elrnrexdm  5383  eufnfv  5465  f1veqaeq  5488  mpt2eq123  5643  ovmpt4g  5702  ovi3  5716  ovg  5718  caovcang  5741  caovcan  5744  frecabcl  6096  nntri3or  6186  dcdifsnid  6195  nnaordex  6216  nnawordex  6217  ereq2  6230  eroveu  6313  2dom  6452  fundmen  6453  xpf1o  6490  nneneq  6503  fisseneq  6567  supsnti  6607  isotilem  6608  updjud  6680  nqtri3or  6858  ltexnqq  6870  aptisr  7227  srpospr  7231  axpre-apti  7323  nntopi  7332  subval  7577  divvalap  8039  nn0ind-raph  8759  frecuzrdgtcl  9708  frecuzrdgfunlem  9715  sqrtrval  10260  divides  10578  dvdstr  10613  odd2np1lem  10652  ndvdssub  10710  eucalglt  10819  hashgcdeq  10984