Theorem eqeq2 2090

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

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

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

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

This theorem is referenced by:  eqeq2i  2091  eqeq2d  2092  eqeq12  2093  eleq1  2141  neeq2  2259  alexeq  2721  ceqex  2722  pm13.183  2732  eqeu  2762  mo2icl  2771  mob2  2772  euind  2779  reu6i  2783  reuind  2795  sbc5  2838  csbiebg  2945  sneq  3409  preqr1g  3558  preqr1  3560  prel12  3563  preq12bg  3565  opth  3992  euotd  4009  ordtriexmid  4265  wetriext  4319  tfisi  4328  ideqg  4505  resieq  4640  cnveqb  4796  cnveq0  4797  iota5  4907  funopg  4954  fneq2  5008  foeq3  5124  tz6.12f  5223  funbrfv  5233  fnbrfvb  5235  fvelimab  5250  elrnrexdm  5327  eufnfv  5410  f1veqaeq  5429  mpt2eq123  5584  ovmpt4g  5643  ovi3  5657  ovg  5659  caovcang  5682  caovcan  5685  nntri3or  6095  nnaordex  6123  nnawordex  6124  ereq2  6137  eroveu  6220  2dom  6308  fundmen  6309  nneneq  6343  supsnti  6418  isotilem  6419  nqtri3or  6586  ltexnqq  6598  aptisr  6955  srpospr  6959  axpre-apti  7051  nntopi  7060  subval  7300  divvalap  7762  nn0ind-raph  8464  frecuzrdgfn  9414  sqrtrval  9886  divides  10197  dvdstr  10232  odd2np1lem  10271  ndvdssub  10330  eucalglt  10439