Theorem oveq1d 5527

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq1d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq1 5519	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1243  (class class class)co 5512

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-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515

This theorem is referenced by:  csbov2g  5546  caovassg  5659  caovdig  5675  caovdirg  5678  caov12d  5682  caov31d  5683  caov411d  5686  grprinvlem  5695  grprinvd  5696  grpridd  5697  caofinvl  5733  omsuc  6051  nnmsucr  6067  nnm1  6097  nnm2  6098  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addasspig  6428  mulasspig  6430  mulpipq2  6469  distrnqg  6485  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  archnqq  6515  prarloclemarch2  6517  enq0sym  6530  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  nqpnq0nq  6551  nq0m0r  6554  nq0a0  6555  nnanq0  6556  distrnq0  6557  addassnq0  6560  addpinq1  6562  prarloclemlo  6592  prarloclem3  6595  prarloclem5  6598  prarloclemcalc  6600  addnqprllem  6625  addnqprulem  6626  appdivnq  6661  recexprlem1ssl  6731  recexprlem1ssu  6732  ltmprr  6740  cauappcvgprlemladdru  6754  cauappcvgprlem1  6757  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemexb  6805  caucvgprprlem1  6807  addcmpblnr  6824  mulcmpblnrlemg  6825  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  ltsrprg  6832  1idsr  6853  pn0sr  6856  recexgt0sr  6858  mulgt0sr  6862  srpospr  6867  prsradd  6870  caucvgsrlemfv  6875  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  caucvgsrlembnd  6885  caucvgsr  6886  pitonnlem1p1  6922  pitonnlem2  6923  pitonn  6924  recidpirqlemcalc  6933  ax1rid  6951  axrnegex  6953  axcnre  6955  recriota  6964  nntopi  6968  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  mul12  7142  mul4  7145  muladd11  7146  readdcan  7153  add12  7169  cnegex  7189  addcan  7191  negeu  7202  pncan2  7218  addsubass  7221  addsub  7222  2addsub  7225  addsubeq4  7226  subid  7230  subid1  7231  npncan  7232  nppcan  7233  nnpcan  7234  nnncan1  7247  npncan3  7249  pnpcan  7250  pnncan  7252  ppncan  7253  addsub4  7254  negsub  7259  subneg  7260  ine0  7391  mulneg1  7392  ltadd2  7416  apreap  7578  cru  7593  recexap  7634  mulcanapd  7642  div23ap  7670  div13ap  7672  divcanap4  7676  divsubdirap  7684  divmuldivap  7688  divdivdivap  7689  divcanap5  7690  divmul13ap  7691  divmuleqap  7693  divdiv32ap  7696  divcanap7  7697  dmdcanap  7698  divdivap1  7699  divdivap2  7700  divadddivap  7703  divsubdivap  7704  conjmulap  7705  divneg2ap  7712  mvllmulapd  7809  lt2mul2div  7845  nndivtr  7955  2halves  8154  halfaddsub  8159  avgle1  8165  avgle2  8166  div4p1lem1div2  8177  un0addcl  8215  un0mulcl  8216  peano2z  8281  zneo  8339  nneoor  8340  nneo  8341  zeo  8343  zeo2  8344  deceq1  8370  qreccl  8576  lincmb01cmp  8871  iccf1o  8872  fzosubel3  9052  2tnp1ge0ge0  9143  fldiv4p1lem1div2  9147  ceilqm1lt  9154  flqdiv  9163  modqlt  9175  modqdiffl  9177  frecuzrdgsuc  9201  frecfzennn  9203  iseqovex  9219  iseq1p  9239  iseqcaopr2  9241  iseqcaopr  9242  iseqid  9247  iseqhomo  9248  expp1  9262  exprecap  9296  expaddzaplem  9298  expmulzap  9301  expdivap  9305  sqval  9312  sqsubswap  9314  subsq  9358  subsq2  9359  binom2  9362  binom2sub  9364  binom3  9366  zesq  9367  bernneq2  9370  reval  9449  crre  9457  remim  9460  remul2  9473  immul2  9480  imval2  9494  cjdivap  9509  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrexlemsqa  9622  resqrexlemex  9623  resqrex  9624  sqrtdiv  9640  absvalsq  9651  absreimsq  9665  absdivap  9668  cau3lem  9710  clim  9802  clim2  9804  climshftlemg  9823  climshft2  9827  climcn1  9829  climcn2  9830  subcn2  9832  climmulc2  9851  climsubc2  9853  clim2iser  9857  climcau  9866  serif0  9871  sqr2irrlem  9877