Theorem eqeq1d 2048

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 2046	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A = C <-> B = C ) )

Syntax hints:   -> wi 4   <-> wb 98   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  sbceq2g  2872  csbhypf  2885  csbiebt  2886  csbiebg  2889  disjssun  3285  sneqrg  3533  preq12b  3541  preq12bg  3544  iin0r  3922  opthg  3975  opeqsn  3989  unisucg  4151  opthreg  4280  tfisi  4310  dmsnopg  4792  relcoi1  4849  iotaeq  4875  iotabi  4876  fneq1  4987  fnun  5005  fnresdisj  5009  fnimadisj  5019  fnimaeq0  5020  sbcfng  5044  foeq1  5102  foco  5116  fvelimab  5229  fvun1  5239  fvmptdv2  5260  fneqeql  5275  dffo3  5314  fvsng  5359  fconstfvm  5379  eufnfv  5389  f1veqaeq  5408  dff13f  5409  f1elima  5412  foeqcnvco  5430  f1eqcocnv  5431  acexmidlemab  5506  eloprabga  5591  ovmpt2dv2  5634  ovi3  5637  ovelimab  5651  caovcang  5662  caovcan  5665  caovimo  5694  grprinvlem  5695  grpridd  5697  suppssfv  5708  suppssov1  5709  caofinvl  5733  op1stg  5777  op2ndg  5778  eqop  5803  reldm  5812  xporderlem  5852  tposfo2  5882  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnm0r  6058  nnmord  6090  nnaordex  6100  nnawordex  6101  ereq1  6113  eqerlem  6137  endisj  6298  fidifsnen  6331  addnidpig  6434  ltexpi  6435  dfplpq2  6452  dfmpq2  6453  recexnq  6488  recmulnqg  6489  ltexnqq  6506  halfnqq  6508  enq0tr  6532  nqnq0pi  6536  addnnnq0  6547  addlocpr  6634  ltexprlemru  6710  ltexpri  6711  lteupri  6715  prplnqu  6718  recexpr  6736  addsrpr  6830  mulsrpr  6831  00sr  6854  negexsr  6857  recexgt0sr  6858  srpospr  6867  prsrriota  6872  caucvgsrlemfv  6875  elrealeu  6906  axrnegex  6953  axprecex  6954  rereceu  6963  recriota  6964  nntopi  6968  axcaucvglemval  6971  axcaucvglemcau  6972  cnegexlem1  7186  cnegex  7189  cnegex2  7190  subval  7203  subadd  7214  subadd2  7215  subsub23  7216  addsubeq4  7226  subcan2  7236  negcon1  7263  subcan  7266  ltadd2  7416  recexre  7569  recexap  7634  muleqadd  7649  receuap  7650  divvalap  7653  divmulap  7654  rec11ap  7686  zdiv  8328  uzin  8505  icc0r  8795  fznlem  8905  fseq1m1p1  8957  1fv  8996  fzon  9022  fvinim0ffz  9096  flqbi  9132  divfl0  9138  modq0  9171  frecuzrdgfn  9198  iseqid3s  9246  iseqid  9247  mulreap  9464  rennim  9600  resqrexlemex  9623  rsqrmo  9625  resqrtcl  9627  rersqrtthlem  9628  sqrtsq2  9641  ialginv  9886  ialgcvga  9890  ialgfx  9891