Theorem eqeq1d 2361

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

Hypothesis

Ref	Expression
eqeq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
eqeq1d	|- (ph -> (A = C <-> B = C))

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 |- (ph -> A = B)
2		eqeq1 2359	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	syl 15	1 |- (ph -> (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  3158  csbhypf  3171  csbiebt  3172  csbiebg  3175  disjssun  3608  sneqrg  3874  preqr2g  4126  preq12b  4127  preq12bg  4128  opkthg  4131  iotaeq  4347  iotabi  4348  eladdci  4399  addcid1  4405  elsuc  4413  addcass  4415  nndisjeq  4429  preaddccan2lem1  4454  tfinltfinlem1  4500  sucoddeven  4511  sfin01  4528  phiall  4618  xpcan  5057  xpcan2  5058  dmsnopg  5066  fneq1  5173  fnun  5189  fnresdisj  5193  fnimadisj  5203  foeq1  5265  foco  5279  fvun1  5379  fvco2  5382  fnasrn  5417  dffo3  5422  fvsng  5446  fconstfv  5456  dff13f  5472  f1fveq  5473  f1elima  5474  ov3  5599  ovelimab  5610  caovcan  5628  caovmo  5645  brcupg  5814  brcomposeg  5819  brdisjg  5821  qsdisj  5995  mapsn  6026  endisj  6051  enadj  6060  enmap2lem3  6065  enmap1lem3  6071  enprmaplem5  6080  enprmaplem6  6081  1cnc  6139  ncdisjeq  6148  addceq0  6219  letc  6231  ce0lenc1  6239  muc0or  6252  csucex  6259  addccan2nclem2  6264  nncdiv3  6277  nnc3n3p1  6278  nchoicelem1  6289  nchoicelem9  6297  nchoicelem14  6302  nchoicelem16  6304  nchoicelem17  6305  nchoice  6308  cantcb  6335