Theorem eqeq1d 2089

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

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:  rspcedeq1vd  2709  sbceq2g  2928  csbhypf  2941  csbiebt  2942  csbiebg  2945  disjssun  3307  sneqrg  3554  preq12b  3562  preq12bg  3565  iin0r  3943  opthg  3993  opeqsn  4007  unisucg  4169  opthreg  4299  tfisi  4328  dmsnopg  4812  relcoi1  4869  iotaeq  4895  iotabi  4896  fneq1  5007  fnun  5025  fnresdisj  5029  fnimadisj  5039  fnimaeq0  5040  sbcfng  5064  foeq1  5122  foco  5136  fvelimab  5250  fvun1  5260  fvmptdv2  5281  fneqeql  5296  dffo3  5335  fvsng  5380  fconstfvm  5400  eufnfv  5410  f1veqaeq  5429  dff13f  5430  f1elima  5433  foeqcnvco  5450  f1eqcocnv  5451  acexmidlemab  5526  eloprabga  5611  ovmpt2dv2  5654  ovi3  5657  ovelimab  5671  caovcang  5682  caovcan  5685  caovimo  5714  grprinvlem  5715  grpridd  5717  suppssfv  5728  suppssov1  5729  caofinvl  5753  op1stg  5797  op2ndg  5798  eqop  5823  reldm  5832  xporderlem  5872  tposfo2  5905  frec0g  6006  frecsuclem3  6013  frecsuc  6014  nnm0r  6081  nnmord  6113  nnaordex  6123  nnawordex  6124  ereq1  6136  eqerlem  6160  endisj  6321  fidifsnen  6355  supelti  6415  pm54.43  6459  addnidpig  6526  ltexpi  6527  dfplpq2  6544  dfmpq2  6545  recexnq  6580  recmulnqg  6581  ltexnqq  6598  halfnqq  6600  enq0tr  6624  nqnq0pi  6628  addnnnq0  6639  addlocpr  6726  ltexprlemru  6802  ltexpri  6803  lteupri  6807  prplnqu  6810  recexpr  6828  addsrpr  6922  mulsrpr  6923  00sr  6946  negexsr  6949  recexgt0sr  6950  srpospr  6959  prsrriota  6964  caucvgsrlemfv  6967  elrealeu  6998  axrnegex  7045  axprecex  7046  rereceu  7055  recriota  7056  nntopi  7060  axcaucvglemval  7063  axcaucvglemcau  7064  cnegexlem1  7283  cnegex  7286  cnegex2  7287  subval  7300  subadd  7311  subadd2  7312  subsub23  7313  addsubeq4  7323  subcan2  7333  negcon1  7360  subcan  7363  addrsub  7475  ltadd2  7523  recexre  7678  recexap  7743  muleqadd  7758  receuap  7759  divvalap  7762  divmulap  7763  rec11ap  7798  zdiv  8435  uzin  8651  icc0r  8949  fznlem  9060  fseq1m1p1  9112  1fv  9149  fzon  9175  fvinim0ffz  9250  ioo0  9268  ico0  9270  ioc0  9271  flqbi  9292  divfl0  9298  modq0  9331  modqmuladdnn0  9370  addmodlteq  9400  frecuzrdgfn  9414  iseqid3s  9466  iseqid  9467  iseqz  9469  mulreap  9751  rennim  9888  resqrexlemex  9911  rsqrmo  9913  resqrtcl  9915  rersqrtthlem  9916  sqrtsq2  9929  divides  10197  dvdsval2  10198  nndivides  10202  dvds0lem  10205  dvds1lem  10206  dvds2lem  10207  negdvdsb  10211  muldvds1  10220  muldvds2  10221  dvdscmulr  10224  dvdsmulcr  10225  dvdstr  10232  dvdsabseq  10247  divconjdvds  10249  odd2np1lem  10271  odd2np1  10272  even2n  10273  oddm1even  10274  2tp1odd  10284  opeo  10297  omeo  10298  m1exp1  10301  divalgb  10325  gcdaddm  10375  gcdabs1  10380  bezout  10400  gcdmultiple  10409  gcdmultiplez  10410  rplpwr  10416  rppwr  10417  ialginv  10429  ialgcvga  10433  ialgfx  10434  eucalgval2  10435  coprmdvds  10474  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  rpexp  10532  rpexp12i  10534  cncongrprm  10536