Theorem eqeq1d 2361

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqeq1d	⊢ (φ → (A = C ↔ B = C))

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (φ → A = B)
2		eqeq1 2359	. 2 ⊢ (A = B → (A = C ↔ B = C))
3	1, 2	syl 15	1 ⊢ (φ → (A = C ↔ B = C))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  sbceq2g  3159  csbhypf  3172  csbiebt  3173  csbiebg  3176  disjssun  3609  sneqrg  3875  preqr2g  4127  preq12b  4128  preq12bg  4129  opkthg  4132  iotaeq  4348  iotabi  4349  eladdci  4400  addcid1  4406  elsuc  4414  addcass  4416  nndisjeq  4430  preaddccan2lem1  4455  tfinltfinlem1  4501  sucoddeven  4512  sfin01  4529  phiall  4619  xpcan  5058  xpcan2  5059  dmsnopg  5067  fneq1  5174  fnun  5190  fnresdisj  5194  fnimadisj  5204  foeq1  5266  foco  5280  fvun1  5380  fvco2  5383  fnasrn  5418  dffo3  5423  fvsng  5447  fconstfv  5457  dff13f  5473  f1fveq  5474  f1elima  5475  ov3  5600  ovelimab  5611  caovcan  5629  caovmo  5646  brcupg  5815  brcomposeg  5820  brdisjg  5822  qsdisj  5996  mapsn  6027  endisj  6052  enadj  6061  enmap2lem3  6066  enmap1lem3  6072  enprmaplem5  6081  enprmaplem6  6082  1cnc  6140  ncdisjeq  6149  addceq0  6220  letc  6232  ce0lenc1  6240  muc0or  6253  csucex  6260  addccan2nclem2  6265  nncdiv3  6278  nnc3n3p1  6279  nchoicelem1  6290  nchoicelem9  6298  nchoicelem14  6303  nchoicelem16  6305  nchoicelem17  6306  nchoice  6309  cantcb  6336