Theorem oveq1d 5857

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 5849	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1343  (class class class)co 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  fvoveq1d  5864  csbov2g  5883  caovassg  6000  caovdig  6016  caovdirg  6019  caov12d  6023  caov31d  6024  caov411d  6027  caofinvl  6072  omsuc  6440  nnmsucr  6456  nnm1  6492  nnm2  6493  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  addasspig  7271  mulasspig  7273  mulpipq2  7312  distrnqg  7328  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltexnqq  7349  archnqq  7358  prarloclemarch2  7360  enq0sym  7373  addnq0mo  7388  mulnq0mo  7389  addnnnq0  7390  nqpnq0nq  7394  nq0m0r  7397  nq0a0  7398  nnanq0  7399  distrnq0  7400  addassnq0  7403  addpinq1  7405  prarloclemlo  7435  prarloclem3  7438  prarloclem5  7441  prarloclemcalc  7443  addnqprllem  7468  addnqprulem  7469  appdivnq  7504  recexprlem1ssl  7574  recexprlem1ssu  7575  ltmprr  7583  cauappcvgprlemladdru  7597  cauappcvgprlem1  7600  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemexb  7648  caucvgprprlem1  7650  addcmpblnr  7680  mulcmpblnrlemg  7681  addsrmo  7684  mulsrmo  7685  addsrpr  7686  mulsrpr  7687  ltsrprg  7688  1idsr  7709  pn0sr  7712  recexgt0sr  7714  mulgt0sr  7719  srpospr  7724  prsradd  7727  caucvgsrlemfv  7732  caucvgsrlemcau  7734  caucvgsrlemgt1  7736  caucvgsrlemoffval  7737  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  caucvgsrlembnd  7742  caucvgsr  7743  map2psrprg  7746  pitonnlem1p1  7787  pitonnlem2  7788  pitonn  7789  recidpirqlemcalc  7798  ax1rid  7818  axrnegex  7820  axcnre  7822  recriota  7831  nntopi  7835  axcaucvglemval  7838  axcaucvglemcau  7839  axcaucvglemres  7840  mul12  8027  mul4  8030  muladd11  8031  readdcan  8038  muladd11r  8054  add12  8056  cnegex  8076  addcan  8078  negeu  8089  pncan2  8105  addsubass  8108  addsub  8109  2addsub  8112  addsubeq4  8113  subid  8117  subid1  8118  npncan  8119  nppcan  8120  nnpcan  8121  nnncan1  8134  npncan3  8136  pnpcan  8137  pnncan  8139  ppncan  8140  addsub4  8141  negsub  8146  subneg  8147  subeqxfrd  8261  mvlraddd  8262  mvlladdd  8263  mvrraddd  8264  subaddeqd  8267  ine0  8292  mulneg1  8293  ltadd2  8317  apreap  8485  cru  8500  recexap  8550  mulcanapd  8558  div23ap  8587  div13ap  8589  divmulassap  8591  divmulasscomap  8592  divcanap4  8595  muldivdirap  8603  divsubdirap  8604  divmuldivap  8608  divdivdivap  8609  divcanap5  8610  divmul13ap  8611  divmuleqap  8613  divdiv32ap  8616  divcanap7  8617  dmdcanap  8618  divdivap1  8619  divdivap2  8620  divadddivap  8623  divsubdivap  8624  conjmulap  8625  divneg2ap  8632  subrecap  8735  mvllmulapd  8738  lt2mul2div  8774  nndivtr  8899  2halves  9086  halfaddsub  9091  avgle1  9097  avgle2  9098  div4p1lem1div2  9110  un0addcl  9147  un0mulcl  9148  peano2z  9227  zneo  9292  nneoor  9293  nneo  9294  zeo  9296  zeo2  9297  deceq1  9326  qreccl  9580  xaddcom  9797  xnegdi  9804  xaddass  9805  xaddass2  9806  xpncan  9807  xleadd1a  9809  xltadd1  9812  xposdif  9818  xadd4d  9821  lincmb01cmp  9939  iccf1o  9940  fz0to4untppr  10059  fzosubel3  10131  qavgle  10194  2tnp1ge0ge0  10236  fldiv4p1lem1div2  10240  ceilqm1lt  10247  flqdiv  10256  modqlt  10268  modqdiffl  10270  modqcyc2  10295  modqaddabs  10297  mulqaddmodid  10299  mulp1mod1  10300  modqmuladd  10301  modqmuladdnn0  10303  qnegmod  10304  addmodid  10307  addmodidr  10308  modqadd2mod  10309  modqm1p1mod0  10310  modqmul12d  10313  modqnegd  10314  modqadd12d  10315  modqsub12d  10316  q2submod  10320  modqmulmodr  10325  modqaddmulmod  10326  modqsubdir  10328  modfzo0difsn  10330  modsumfzodifsn  10331  addmodlteq  10333  frecuzrdgsuc  10349  frecfzennn  10361  iseqovex  10391  seq3-1p  10415  seq3caopr2  10417  seq3caopr  10418  seq3id  10443  seq3homo  10445  seq3z  10446  expp1  10462  exprecap  10496  expaddzaplem  10498  expmulzap  10501  expdivap  10506  sqval  10513  sqsubswap  10515  subsq  10561  subsq2  10562  binom2  10566  binom2sub  10568  mulbinom2  10571  binom3  10572  zesq  10573  bernneq2  10576  modqexp  10581  sqoddm1div8  10608  nn0opthlem1d  10633  nn0opthd  10635  nn0opth2d  10636  facp1  10643  facdiv  10651  facndiv  10652  faclbnd  10654  faclbnd2  10655  faclbnd3  10656  bcval  10662  bccmpl  10667  bcm1k  10673  bcp1n  10674  bcp1nk  10675  bcval5  10676  bcp1m1  10678  bcpasc  10679  bcn2m1  10682  hashprg  10721  hashdifpr  10733  hashfzo  10735  hashfzp1  10737  hashfz0  10738  hashxp  10739  zfz1isolemsplit  10751  zfz1isolem1  10753  seq3coll  10755  reval  10791  crre  10799  remim  10802  remul2  10815  immul2  10822  imval2  10836  cjdivap  10851  caucvgre  10923  cvg1nlemcau  10926  cvg1nlemres  10927  resqrexlemp1rp  10948  resqrexlemfp1  10951  resqrexlemover  10952  resqrexlemcalc1  10956  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  resqrexlemsqa  10966  resqrexlemex  10967  resqrex  10968  sqrtdiv  10984  absvalsq  10995  absreimsq  11009  absdivap  11012  cau3lem  11056  maxabslemlub  11149  maxabslemval  11150  max0addsup  11161  minabs  11177  bdtrilem  11180  bdtri  11181  xrmaxaddlem  11201  xrmaxadd  11202  xrbdtri  11217  clim  11222  clim2  11224  climshftlemg  11243  climshft2  11247  climcn1  11249  climcn2  11250  subcn2  11252  reccn2ap  11254  climmulc2  11272  climsubc2  11274  clim2ser  11278  iser3shft  11287  climcau  11288  serf0  11293  fzosump1  11358  fsum1p  11359  fsump1  11361  sumsplitdc  11373  fsump1i  11374  mptfzshft  11383  fisum0diag2  11388  fsumconst  11395  fsumdifsnconst  11396  modfsummodlemstep  11398  modfsummod  11399  telfsumo  11407  fsumparts  11411  fsumrelem  11412  hash2iun1dif1  11421  binomlem  11424  binom  11425  binom1p  11426  binom1dif  11428  bcxmas  11430  isumsplit  11432  isum1p  11433  arisum  11439  arisum2  11440  trireciplem  11441  geoserap  11448  geolim  11452  geolim2  11453  georeclim  11454  geo2sum  11455  geoisum1  11460  cvgratnnlemseq  11467  cvgratnnlemsumlt  11469  cvgratnnlemfm  11470  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  fprod1p  11540  fprodp1  11541  fprodcl2lem  11546  fprodfac  11556  fprodeq0  11558  fprodconst  11561  fprodrec  11570  fprodsplit1f  11575  fprodmodd  11582  efcllemp  11599  ef0lem  11601  efval  11602  esum  11603  ege2le3  11612  efaddlem  11615  efsep  11632  effsumlt  11633  eft0val  11634  efgt1p2  11636  efgt1p  11637  sinval  11643  cosval  11644  resinval  11656  recosval  11657  efi4p  11658  resin4p  11659  recos4p  11660  sinneg  11667  cosneg  11668  efival  11673  sinadd  11677  cosadd  11678  tanaddap  11680  sinmul  11685  cosmul  11686  cos2t  11691  cos2tsin  11692  ef01bndlem  11697  absefib  11711  demoivre  11713  demoivreALT  11714  eirraplem  11717  p1modz1  11734  dvdsmodexp  11735  moddvds  11739  mulmoddvds  11801  3dvds2dec  11803  zeo3  11805  odd2np1lem  11809  odd2np1  11810  oexpneg  11814  2tp1odd  11821  ltoddhalfle  11830  opoe  11832  opeo  11834  omeo  11835  m1expo  11837  m1exp1  11838  nn0o1gt2  11842  nn0o  11844  divalglemnn  11855  divalglemqt  11856  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  flodddiv4  11871  flodddiv4t2lthalf  11874  gcdaddm  11917  bezoutlemnewy  11929  bezoutlema  11932  bezoutlemb  11933  bezoutlemex  11934  bezoutlemaz  11936  mulgcd  11949  gcddiv  11952  gcdmultiplez  11954  rpmulgcd  11959  rplpwr  11960  uzwodc  11970  lcmgcdlem  12009  lcmgcd  12010  divgcdcoprmex  12034  cncongr2  12036  prmexpb  12083  rpexp  12085  rpexp1i  12086  sqrt2irrlem  12093  oddpwdclemxy  12101  oddpwdclemndvds  12103  sqpweven  12107  2sqpwodd  12108  sqne2sq  12109  qmuldeneqnum  12127  nn0gcdsq  12132  zgcdsq  12133  numdensq  12134  dfphi2  12152  phiprmpw  12154  phiprm  12155  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  fermltl  12166  prmdiv  12167  prmdiveq  12168  prmdivdiv  12169  hashgcdlem  12170  odzval  12173  odzcllem  12174  odzdvds  12177  vfermltl  12183  powm2modprm  12184  reumodprminv  12185  modprm0  12186  nnnn0modprm0  12187  modprmn0modprm0  12188  coprimeprodsq  12189  coprimeprodsq2  12190  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem4  12200  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem15  12210  pythagtriplem16  12211  pythagtriplem17  12212  pythagtriplem18  12213  pceu  12227  pczpre  12229  pcdiv  12234  pcqdiv  12239  pcrec  12240  pczndvds  12247  pcneg  12256  pc2dvds  12261  pcprmpw2  12264  pcaddlem  12270  pcadd  12271  fldivp1  12278  pockthlem  12286  pockthi  12288  4sqlem5  12312  4sqlem9  12316  4sqlem10  12317  4sqlem2  12319  4sqlem3  12320  4sqlem4  12322  mul4sqlem  12323  ennnfonelemkh  12345  ennnfonelemhf1o  12346  grprinvlem  12616  grprinvd  12617  grpridd  12618  resttop  12810  restco  12814  restin  12816  lmfval  12832  cnprcl2k  12846  txrest  12916  txdis1cn  12918  cnmpt2res  12937  psmettri2  12968  psmettri  12970  xmettri2  13001  xmettri  13012  mettri  13013  metrtri  13017  blvalps  13028  blval  13029  xblss2  13045  blhalf  13048  comet  13139  xmetxp  13147  txmetcnp  13158  cnmet  13170  ioo2bl  13183  limcmpted  13272  limcimolemlt  13273  cnplimclemr  13278  limccnp2cntop  13286  reldvg  13288  dvfvalap  13290  dvidlemap  13300  dvconst  13301  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvexp  13315  dvrecap  13317  dvmptcmulcn  13323  dveflem  13327  sin0pilem1  13342  sinperlem  13369  ptolemy  13385  tangtx  13399  abssinper  13407  reexplog  13432  relogexp  13433  cxprec  13471  rpdivcxp  13472  cxpmul  13473  rpabscxpbnd  13499  rplogbval  13503  rplogbreexp  13511  rprelogbmul  13513  logbrec  13518  logbgcd1irraplemap  13527  binom4  13537  lgslem1  13541  lgslem4  13544  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  lgsval4lem  13552  lgsvalmod  13560  lgsneg  13565  lgsneg1  13566  lgsmod  13567  lgsdilem  13568  lgsdir2lem4  13572  lgsdir2  13574  lgsdirprm  13575  lgsdir  13576  lgsne0  13579  lgssq  13581  lgssq2  13582  lgsmulsqcoprm  13587  lgsdirnn0  13588  lgsdinn0  13589  2sqlem1  13590  2sqlem2  13591  mul2sq  13592  2sqlem3  13593  2sqlem4  13594  2sqlem8  13599  2sqlem9  13600  2sqlem10  13601  trilpolemeq1  13919  trilpolemlt1  13920  trirec0xor  13924  apdifflemf  13925  apdiff  13927