Theorem oveq1d 5868

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

Syntax hints:   → wi 4   = wceq 1348  (class class class)co 5853

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  fvoveq1d  5875  csbov2g  5894  caovassg  6011  caovdig  6027  caovdirg  6030  caov12d  6034  caov31d  6035  caov411d  6038  caofinvl  6083  omsuc  6451  nnmsucr  6467  nnm1  6504  nnm2  6505  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  addasspig  7292  mulasspig  7294  mulpipq2  7333  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  archnqq  7379  prarloclemarch2  7381  enq0sym  7394  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  nqpnq0nq  7415  nq0m0r  7418  nq0a0  7419  nnanq0  7420  distrnq0  7421  addassnq0  7424  addpinq1  7426  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  prarloclemcalc  7464  addnqprllem  7489  addnqprulem  7490  appdivnq  7525  recexprlem1ssl  7595  recexprlem1ssu  7596  ltmprr  7604  cauappcvgprlemladdru  7618  cauappcvgprlem1  7621  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemexb  7669  caucvgprprlem1  7671  addcmpblnr  7701  mulcmpblnrlemg  7702  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  ltsrprg  7709  1idsr  7730  pn0sr  7733  recexgt0sr  7735  mulgt0sr  7740  srpospr  7745  prsradd  7748  caucvgsrlemfv  7753  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffval  7758  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  caucvgsrlembnd  7763  caucvgsr  7764  map2psrprg  7767  pitonnlem1p1  7808  pitonnlem2  7809  pitonn  7810  recidpirqlemcalc  7819  ax1rid  7839  axrnegex  7841  axcnre  7843  recriota  7852  nntopi  7856  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  mul12  8048  mul4  8051  muladd11  8052  readdcan  8059  muladd11r  8075  add12  8077  cnegex  8097  addcan  8099  negeu  8110  pncan2  8126  addsubass  8129  addsub  8130  2addsub  8133  addsubeq4  8134  subid  8138  subid1  8139  npncan  8140  nppcan  8141  nnpcan  8142  nnncan1  8155  npncan3  8157  pnpcan  8158  pnncan  8160  ppncan  8161  addsub4  8162  negsub  8167  subneg  8168  subeqxfrd  8282  mvlraddd  8283  mvlladdd  8284  mvrraddd  8285  subaddeqd  8288  ine0  8313  mulneg1  8314  ltadd2  8338  apreap  8506  cru  8521  recexap  8571  mulcanapd  8579  div23ap  8608  div13ap  8610  divmulassap  8612  divmulasscomap  8613  divcanap4  8616  muldivdirap  8624  divsubdirap  8625  divmuldivap  8629  divdivdivap  8630  divcanap5  8631  divmul13ap  8632  divmuleqap  8634  divdiv32ap  8637  divcanap7  8638  dmdcanap  8639  divdivap1  8640  divdivap2  8641  divadddivap  8644  divsubdivap  8645  conjmulap  8646  divneg2ap  8653  subrecap  8756  mvllmulapd  8759  lt2mul2div  8795  nndivtr  8920  2halves  9107  halfaddsub  9112  avgle1  9118  avgle2  9119  div4p1lem1div2  9131  un0addcl  9168  un0mulcl  9169  peano2z  9248  zneo  9313  nneoor  9314  nneo  9315  zeo  9317  zeo2  9318  deceq1  9347  qreccl  9601  xaddcom  9818  xnegdi  9825  xaddass  9826  xaddass2  9827  xpncan  9828  xleadd1a  9830  xltadd1  9833  xposdif  9839  xadd4d  9842  lincmb01cmp  9960  iccf1o  9961  fz0to4untppr  10080  fzosubel3  10152  qavgle  10215  2tnp1ge0ge0  10257  fldiv4p1lem1div2  10261  ceilqm1lt  10268  flqdiv  10277  modqlt  10289  modqdiffl  10291  modqcyc2  10316  modqaddabs  10318  mulqaddmodid  10320  mulp1mod1  10321  modqmuladd  10322  modqmuladdnn0  10324  qnegmod  10325  addmodid  10328  addmodidr  10329  modqadd2mod  10330  modqm1p1mod0  10331  modqmul12d  10334  modqnegd  10335  modqadd12d  10336  modqsub12d  10337  q2submod  10341  modqmulmodr  10346  modqaddmulmod  10347  modqsubdir  10349  modfzo0difsn  10351  modsumfzodifsn  10352  addmodlteq  10354  frecuzrdgsuc  10370  frecfzennn  10382  iseqovex  10412  seq3-1p  10436  seq3caopr2  10438  seq3caopr  10439  seq3id  10464  seq3homo  10466  seq3z  10467  expp1  10483  exprecap  10517  expaddzaplem  10519  expmulzap  10522  expdivap  10527  sqval  10534  sqsubswap  10536  subsq  10582  subsq2  10583  binom2  10587  binom2sub  10589  mulbinom2  10592  binom3  10593  zesq  10594  bernneq2  10597  modqexp  10602  sqoddm1div8  10629  nn0opthlem1d  10654  nn0opthd  10656  nn0opth2d  10657  facp1  10664  facdiv  10672  facndiv  10673  faclbnd  10675  faclbnd2  10676  faclbnd3  10677  bcval  10683  bccmpl  10688  bcm1k  10694  bcp1n  10695  bcp1nk  10696  bcval5  10697  bcp1m1  10699  bcpasc  10700  bcn2m1  10703  hashprg  10743  hashdifpr  10755  hashfzo  10757  hashfzp1  10759  hashfz0  10760  hashxp  10761  zfz1isolemsplit  10773  zfz1isolem1  10775  seq3coll  10777  reval  10813  crre  10821  remim  10824  remul2  10837  immul2  10844  imval2  10858  cjdivap  10873  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  resqrexlemsqa  10988  resqrexlemex  10989  resqrex  10990  sqrtdiv  11006  absvalsq  11017  absreimsq  11031  absdivap  11034  cau3lem  11078  maxabslemlub  11171  maxabslemval  11172  max0addsup  11183  minabs  11199  bdtrilem  11202  bdtri  11203  xrmaxaddlem  11223  xrmaxadd  11224  xrbdtri  11239  clim  11244  clim2  11246  climshftlemg  11265  climshft2  11269  climcn1  11271  climcn2  11272  subcn2  11274  reccn2ap  11276  climmulc2  11294  climsubc2  11296  clim2ser  11300  iser3shft  11309  climcau  11310  serf0  11315  fzosump1  11380  fsum1p  11381  fsump1  11383  sumsplitdc  11395  fsump1i  11396  mptfzshft  11405  fisum0diag2  11410  fsumconst  11417  fsumdifsnconst  11418  modfsummodlemstep  11420  modfsummod  11421  telfsumo  11429  fsumparts  11433  fsumrelem  11434  hash2iun1dif1  11443  binomlem  11446  binom  11447  binom1p  11448  binom1dif  11450  bcxmas  11452  isumsplit  11454  isum1p  11455  arisum  11461  arisum2  11462  trireciplem  11463  geoserap  11470  geolim  11474  geolim2  11475  georeclim  11476  geo2sum  11477  geoisum1  11482  cvgratnnlemseq  11489  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  fprod1p  11562  fprodp1  11563  fprodcl2lem  11568  fprodfac  11578  fprodeq0  11580  fprodconst  11583  fprodrec  11592  fprodsplit1f  11597  fprodmodd  11604  efcllemp  11621  ef0lem  11623  efval  11624  esum  11625  ege2le3  11634  efaddlem  11637  efsep  11654  effsumlt  11655  eft0val  11656  efgt1p2  11658  efgt1p  11659  sinval  11665  cosval  11666  resinval  11678  recosval  11679  efi4p  11680  resin4p  11681  recos4p  11682  sinneg  11689  cosneg  11690  efival  11695  sinadd  11699  cosadd  11700  tanaddap  11702  sinmul  11707  cosmul  11708  cos2t  11713  cos2tsin  11714  ef01bndlem  11719  absefib  11733  demoivre  11735  demoivreALT  11736  eirraplem  11739  p1modz1  11756  dvdsmodexp  11757  moddvds  11761  mulmoddvds  11823  3dvds2dec  11825  zeo3  11827  odd2np1lem  11831  odd2np1  11832  oexpneg  11836  2tp1odd  11843  ltoddhalfle  11852  opoe  11854  opeo  11856  omeo  11857  m1expo  11859  m1exp1  11860  nn0o1gt2  11864  nn0o  11866  divalglemnn  11877  divalglemqt  11878  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  flodddiv4  11893  flodddiv4t2lthalf  11896  gcdaddm  11939  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  bezoutlemex  11956  bezoutlemaz  11958  mulgcd  11971  gcddiv  11974  gcdmultiplez  11976  rpmulgcd  11981  rplpwr  11982  uzwodc  11992  lcmgcdlem  12031  lcmgcd  12032  divgcdcoprmex  12056  cncongr2  12058  prmexpb  12105  rpexp  12107  rpexp1i  12108  sqrt2irrlem  12115  oddpwdclemxy  12123  oddpwdclemndvds  12125  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  qmuldeneqnum  12149  nn0gcdsq  12154  zgcdsq  12155  numdensq  12156  dfphi2  12174  phiprmpw  12176  phiprm  12177  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  fermltl  12188  prmdiv  12189  prmdiveq  12190  prmdivdiv  12191  hashgcdlem  12192  odzval  12195  odzcllem  12196  odzdvds  12199  vfermltl  12205  powm2modprm  12206  reumodprminv  12207  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  coprimeprodsq  12211  coprimeprodsq2  12212  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  pythagtriplem18  12235  pceu  12249  pczpre  12251  pcdiv  12256  pcqdiv  12261  pcrec  12262  pczndvds  12269  pcneg  12278  pc2dvds  12283  pcprmpw2  12286  pcaddlem  12292  pcadd  12293  fldivp1  12300  pockthlem  12308  pockthi  12310  4sqlem5  12334  4sqlem9  12338  4sqlem10  12339  4sqlem2  12341  4sqlem3  12342  4sqlem4  12344  mul4sqlem  12345  ennnfonelemkh  12367  ennnfonelemhf1o  12368  grprinvlem  12639  grprinvd  12640  grpridd  12641  isnsgrp  12647  sgrpass  12649  sgrp1  12651  mnd12g  12664  mndpropd  12676  mhmlin  12690  grprcan  12740  grpinvid1  12754  isgrpinv  12756  grplcan  12761  grpasscan1  12762  resttop  12964  restco  12968  restin  12970  lmfval  12986  cnprcl2k  13000  txrest  13070  txdis1cn  13072  cnmpt2res  13091  psmettri2  13122  psmettri  13124  xmettri2  13155  xmettri  13166  mettri  13167  metrtri  13171  blvalps  13182  blval  13183  xblss2  13199  blhalf  13202  comet  13293  xmetxp  13301  txmetcnp  13312  cnmet  13324  ioo2bl  13337  limcmpted  13426  limcimolemlt  13427  cnplimclemr  13432  limccnp2cntop  13440  reldvg  13442  dvfvalap  13444  dvidlemap  13454  dvconst  13455  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvexp  13469  dvrecap  13471  dvmptcmulcn  13477  dveflem  13481  sin0pilem1  13496  sinperlem  13523  ptolemy  13539  tangtx  13553  abssinper  13561  reexplog  13586  relogexp  13587  cxprec  13625  rpdivcxp  13626  cxpmul  13627  rpabscxpbnd  13653  rplogbval  13657  rplogbreexp  13665  rprelogbmul  13667  logbrec  13672  logbgcd1irraplemap  13681  binom4  13691  lgslem1  13695  lgslem4  13698  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsval4lem  13706  lgsvalmod  13714  lgsneg  13719  lgsneg1  13720  lgsmod  13721  lgsdilem  13722  lgsdir2lem4  13726  lgsdir2  13728  lgsdirprm  13729  lgsdir  13730  lgsne0  13733  lgssq  13735  lgssq2  13736  lgsmulsqcoprm  13741  lgsdirnn0  13742  lgsdinn0  13743  2sqlem1  13744  2sqlem2  13745  mul2sq  13746  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  2sqlem9  13754  2sqlem10  13755  trilpolemeq1  14072  trilpolemlt1  14073  trirec0xor  14077  apdifflemf  14078  apdiff  14080