Theorem oveq1d 5915

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

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveq1d	|- ( ph -> ( A F C ) = ( B F C ) )

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq1 5907	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1364  (class class class)co 5900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-br 4022  df-iota 5199  df-fv 5246  df-ov 5903

This theorem is referenced by:  fvoveq1d  5922  csbov2g  5941  caovassg  6059  caovdig  6075  caovdirg  6078  caov12d  6082  caov31d  6083  caov411d  6086  caofinvl  6133  omsuc  6501  nnmsucr  6517  nnm1  6554  nnm2  6555  ecovass  6674  ecoviass  6675  ecovdi  6676  ecovidi  6677  addasspig  7364  mulasspig  7366  mulpipq2  7405  distrnqg  7421  ltsonq  7432  ltanqg  7434  ltmnqg  7435  ltexnqq  7442  archnqq  7451  prarloclemarch2  7453  enq0sym  7466  addnq0mo  7481  mulnq0mo  7482  addnnnq0  7483  nqpnq0nq  7487  nq0m0r  7490  nq0a0  7491  nnanq0  7492  distrnq0  7493  addassnq0  7496  addpinq1  7498  prarloclemlo  7528  prarloclem3  7531  prarloclem5  7534  prarloclemcalc  7536  addnqprllem  7561  addnqprulem  7562  appdivnq  7597  recexprlem1ssl  7667  recexprlem1ssu  7668  ltmprr  7676  cauappcvgprlemladdru  7690  cauappcvgprlem1  7693  caucvgprlemnkj  7700  caucvgprlemnbj  7701  caucvgprlemcl  7710  caucvgprlemladdfu  7711  caucvgprlemladdrl  7712  caucvgprlem1  7713  caucvgprprlemcbv  7721  caucvgprprlemval  7722  caucvgprprlemexb  7741  caucvgprprlem1  7743  addcmpblnr  7773  mulcmpblnrlemg  7774  addsrmo  7777  mulsrmo  7778  addsrpr  7779  mulsrpr  7780  ltsrprg  7781  1idsr  7802  pn0sr  7805  recexgt0sr  7807  mulgt0sr  7812  srpospr  7817  prsradd  7820  caucvgsrlemfv  7825  caucvgsrlemcau  7827  caucvgsrlemgt1  7829  caucvgsrlemoffval  7830  caucvgsrlemoffcau  7832  caucvgsrlemoffres  7834  caucvgsrlembnd  7835  caucvgsr  7836  map2psrprg  7839  pitonnlem1p1  7880  pitonnlem2  7881  pitonn  7882  recidpirqlemcalc  7891  ax1rid  7911  axrnegex  7913  axcnre  7915  recriota  7924  nntopi  7928  axcaucvglemval  7931  axcaucvglemcau  7932  axcaucvglemres  7933  mul12  8121  mul4  8124  muladd11  8125  readdcan  8132  muladd11r  8148  add12  8150  cnegex  8170  addcan  8172  negeu  8183  pncan2  8199  addsubass  8202  addsub  8203  2addsub  8206  addsubeq4  8207  subid  8211  subid1  8212  npncan  8213  nppcan  8214  nnpcan  8215  nnncan1  8228  npncan3  8230  pnpcan  8231  pnncan  8233  ppncan  8234  addsub4  8235  negsub  8240  subneg  8241  subeqxfrd  8355  mvlraddd  8356  mvlladdd  8357  mvrraddd  8358  subaddeqd  8361  ine0  8386  mulneg1  8387  ltadd2  8411  apreap  8579  cru  8594  recexap  8645  mulcanapd  8653  div23ap  8683  div13ap  8685  divmulassap  8687  divmulasscomap  8688  divcanap4  8691  muldivdirap  8699  divsubdirap  8700  divmuldivap  8704  divdivdivap  8705  divcanap5  8706  divmul13ap  8707  divmuleqap  8709  divdiv32ap  8712  divcanap7  8713  dmdcanap  8714  divdivap1  8715  divdivap2  8716  divadddivap  8719  divsubdivap  8720  conjmulap  8721  divneg2ap  8728  subrecap  8831  mvllmulapd  8834  lt2mul2div  8871  nndivtr  8996  2halves  9183  halfaddsub  9188  avgle1  9194  avgle2  9195  div4p1lem1div2  9207  un0addcl  9244  un0mulcl  9245  peano2z  9324  zneo  9389  nneoor  9390  nneo  9391  zeo  9393  zeo2  9394  deceq1  9423  qreccl  9678  xaddcom  9897  xnegdi  9904  xaddass  9905  xaddass2  9906  xpncan  9907  xleadd1a  9909  xltadd1  9912  xposdif  9918  xadd4d  9921  lincmb01cmp  10039  iccf1o  10040  fz0to4untppr  10160  fzosubel3  10232  qavgle  10295  2tnp1ge0ge0  10338  fldiv4p1lem1div2  10342  ceilqm1lt  10349  flqdiv  10358  modqlt  10370  modqdiffl  10372  modqcyc2  10397  modqaddabs  10399  mulqaddmodid  10401  mulp1mod1  10402  modqmuladd  10403  modqmuladdnn0  10405  qnegmod  10406  addmodid  10409  addmodidr  10410  modqadd2mod  10411  modqm1p1mod0  10412  modqmul12d  10415  modqnegd  10416  modqadd12d  10417  modqsub12d  10418  q2submod  10422  modqmulmodr  10427  modqaddmulmod  10428  modqsubdir  10430  modfzo0difsn  10432  modsumfzodifsn  10433  addmodlteq  10435  frecuzrdgsuc  10451  frecfzennn  10463  iseqovex  10495  seq3-1p  10519  seq3caopr2  10521  seq3caopr  10522  seq3id  10547  seq3homo  10549  seq3z  10550  seqfeq4g  10552  expp1  10567  exprecap  10601  expaddzaplem  10603  expmulzap  10606  expdivap  10611  sqval  10618  sqsubswap  10620  sqdividap  10625  subsq  10667  subsq2  10668  binom2  10672  binom2sub  10674  mulbinom2  10677  binom3  10678  zesq  10679  bernneq2  10682  modqexp  10687  sqoddm1div8  10714  mulsubdivbinom2ap  10732  nn0opthlem1d  10741  nn0opthd  10743  nn0opth2d  10744  facp1  10751  facdiv  10759  facndiv  10760  faclbnd  10762  faclbnd2  10763  faclbnd3  10764  bcval  10770  bccmpl  10775  bcm1k  10781  bcp1n  10782  bcp1nk  10783  bcval5  10784  bcp1m1  10786  bcpasc  10787  bcn2m1  10790  hashprg  10829  hashdifpr  10841  hashfzo  10843  hashfzp1  10845  hashfz0  10846  hashxp  10847  zfz1isolemsplit  10859  zfz1isolem1  10861  seq3coll  10863  reval  10899  crre  10907  remim  10910  remul2  10923  immul2  10930  imval2  10944  cjdivap  10959  caucvgre  11031  cvg1nlemcau  11034  cvg1nlemres  11035  resqrexlemp1rp  11056  resqrexlemfp1  11059  resqrexlemover  11060  resqrexlemcalc1  11064  resqrexlemcalc3  11066  resqrexlemnm  11068  resqrexlemoverl  11071  resqrexlemglsq  11072  resqrexlemga  11073  resqrexlemsqa  11074  resqrexlemex  11075  resqrex  11076  sqrtdiv  11092  absvalsq  11103  absreimsq  11117  absdivap  11120  cau3lem  11164  maxabslemlub  11257  maxabslemval  11258  max0addsup  11269  minabs  11285  bdtrilem  11288  bdtri  11289  xrmaxaddlem  11309  xrmaxadd  11310  xrbdtri  11325  clim  11330  clim2  11332  climshftlemg  11351  climshft2  11355  climcn1  11357  climcn2  11358  subcn2  11360  reccn2ap  11362  climmulc2  11380  climsubc2  11382  clim2ser  11386  iser3shft  11395  climcau  11396  serf0  11401  fzosump1  11466  fsum1p  11467  fsump1  11469  sumsplitdc  11481  fsump1i  11482  mptfzshft  11491  fisum0diag2  11496  fsumconst  11503  fsumdifsnconst  11504  modfsummodlemstep  11506  modfsummod  11507  telfsumo  11515  fsumparts  11519  fsumrelem  11520  hash2iun1dif1  11529  binomlem  11532  binom  11533  binom1p  11534  binom1dif  11536  bcxmas  11538  isumsplit  11540  isum1p  11541  arisum  11547  arisum2  11548  trireciplem  11549  geoserap  11556  geolim  11560  geolim2  11561  georeclim  11562  geo2sum  11563  geoisum1  11568  cvgratnnlemseq  11575  cvgratnnlemsumlt  11577  cvgratnnlemfm  11578  cvgratz  11581  mertenslemi1  11584  mertenslem2  11585  mertensabs  11586  fprod1p  11648  fprodp1  11649  fprodcl2lem  11654  fprodfac  11664  fprodeq0  11666  fprodconst  11669  fprodrec  11678  fprodsplit1f  11683  fprodmodd  11690  efcllemp  11707  ef0lem  11709  efval  11710  esum  11711  ege2le3  11720  efaddlem  11723  efsep  11740  effsumlt  11741  eft0val  11742  efgt1p2  11744  efgt1p  11745  sinval  11751  cosval  11752  resinval  11764  recosval  11765  efi4p  11766  resin4p  11767  recos4p  11768  sinneg  11775  cosneg  11776  efival  11781  sinadd  11785  cosadd  11786  tanaddap  11788  sinmul  11793  cosmul  11794  cos2t  11799  cos2tsin  11800  ef01bndlem  11805  absefib  11819  demoivre  11821  demoivreALT  11822  eirraplem  11825  p1modz1  11842  dvdsmodexp  11843  moddvds  11847  mulmoddvds  11910  3dvds2dec  11912  zeo3  11914  odd2np1lem  11918  odd2np1  11919  oexpneg  11923  2tp1odd  11930  ltoddhalfle  11939  opoe  11941  opeo  11943  omeo  11944  m1expo  11946  m1exp1  11947  nn0o1gt2  11951  nn0o  11953  divalglemnn  11964  divalglemqt  11965  divalglemeunn  11967  divalglemex  11968  divalglemeuneg  11969  flodddiv4  11980  flodddiv4t2lthalf  11983  gcdaddm  12026  bezoutlemnewy  12038  bezoutlema  12041  bezoutlemb  12042  bezoutlemex  12043  bezoutlemaz  12045  mulgcd  12058  gcddiv  12061  gcdmultiplez  12063  rpmulgcd  12068  rplpwr  12069  uzwodc  12079  lcmgcdlem  12120  lcmgcd  12121  divgcdcoprmex  12145  cncongr2  12147  prmexpb  12194  rpexp  12196  rpexp1i  12197  sqrt2irrlem  12204  oddpwdclemxy  12212  oddpwdclemndvds  12214  sqpweven  12218  2sqpwodd  12219  sqne2sq  12220  qmuldeneqnum  12238  nn0gcdsq  12243  zgcdsq  12244  numdensq  12245  dfphi2  12263  phiprmpw  12265  phiprm  12266  eulerthlema  12273  eulerthlemh  12274  eulerthlemth  12275  fermltl  12277  prmdiv  12278  prmdiveq  12279  prmdivdiv  12280  hashgcdlem  12281  odzval  12284  odzcllem  12285  odzdvds  12288  vfermltl  12294  powm2modprm  12295  reumodprminv  12296  modprm0  12297  nnnn0modprm0  12298  modprmn0modprm0  12299  coprimeprodsq  12300  coprimeprodsq2  12301  pythagtriplem1  12308  pythagtriplem3  12310  pythagtriplem4  12311  pythagtriplem6  12313  pythagtriplem7  12314  pythagtriplem12  12318  pythagtriplem14  12320  pythagtriplem15  12321  pythagtriplem16  12322  pythagtriplem17  12323  pythagtriplem18  12324  pceu  12338  pczpre  12340  pcdiv  12345  pcqdiv  12350  pcrec  12351  pczndvds  12359  pcneg  12368  pc2dvds  12373  pcprmpw2  12376  pcaddlem  12382  pcadd  12383  fldivp1  12391  pockthlem  12399  pockthi  12401  4sqlem5  12425  4sqlem9  12429  4sqlem10  12430  4sqlem2  12432  4sqlem3  12433  4sqlem4  12435  mul4sqlem  12436  4sqlem11  12444  4sqlem12  12445  4sqlem14  12447  4sqlem15  12448  4sqlem17  12450  4sqlem19  12452  ennnfonelemkh  12474  ennnfonelemhf1o  12475  setscomd  12564  ressressg  12598  qusex  12813  qusin  12814  grpinvalem  12872  grpinva  12873  grprida  12874  gsumsplit1r  12884  isnsgrp  12892  sgrpass  12894  sgrp1  12897  sgrppropd  12899  mnd12g  12912  mndpropd  12924  mhmex  12937  mhmlin  12942  grprcan  13004  grpinvid1  13019  isgrpinv  13021  grplcan  13029  grpasscan1  13030  grplmulf1o  13041  grpinvadd  13045  grpinvsub  13049  grpsubsub4  13060  grppnpcan2  13061  grpnpncan  13062  dfgrp3mlem  13065  dfgrp3m  13066  grplactcnv  13069  imasgrp2  13075  mhmlem  13079  mhmid  13080  mhmmnd  13081  mulgnnp1  13095  mulg2  13096  mulgnn0p1  13098  mulgsubcl  13101  mulgneg  13105  mulgaddcomlem  13110  mulgaddcom  13111  mulgz  13115  mulgnn0dir  13117  mulgdirlem  13118  mulgdir  13119  mulgneg2  13121  mulgnnass  13122  mulgnn0ass  13123  mulgass  13124  mulgassr  13125  mulgmodid  13126  mulgsubdir  13127  isnsg3  13171  nmzsubg  13174  ssnmz  13175  0nsg  13178  eqger  13188  eqgid  13190  eqgcpbl  13192  ghmlin  13212  ghmmulg  13220  ghmnsgima  13232  ghmnsgpreima  13233  conjghm  13240  conjnmz  13243  ablsub2inv  13275  abladdsub4  13278  abladdsub  13279  ablpncan2  13280  ablpnpcan  13284  ablnncan  13285  ablnnncan1  13288  mgpress  13310  rngass  13318  rngdi  13319  rngdir  13320  rnglz  13324  rngmneg1  13326  rngsubdir  13331  rngpropd  13334  imasrng  13335  srgass  13350  srgmulgass  13368  srgpcomp  13369  srgpcompp  13370  srgpcomppsc  13371  ringpropd  13417  ringlz  13422  ring1eq0  13425  ringnegl  13428  ringmneg1  13430  ringsubdir  13434  mulgass2  13435  ring1  13436  imasring  13439  opprrng  13452  opprring  13454  unitgrp  13491  dvrcan1  13515  rdivmuldivd  13519  subrginv  13609  islmod  13632  lmodlema  13633  islmodd  13634  lmod0vs  13662  lmodvs0  13663  lmodvsmmulgdi  13664  lmodvneg1  13671  lmodvsneg  13672  lmodsubvs  13684  lmodsubdi  13685  lmodsubdir  13686  lmodprop2d  13689  rmodislmodlem  13691  rmodislmod  13692  lsssetm  13697  islssmd  13700  lssclg  13705  lssvacl  13706  lss1d  13724  lsspropdg  13772  sraval  13778  rnglidlmcl  13821  resttop  14155  restco  14159  restin  14161  lmfval  14177  cnprcl2k  14191  txrest  14261  txdis1cn  14263  cnmpt2res  14282  psmettri2  14313  psmettri  14315  xmettri2  14346  xmettri  14357  mettri  14358  metrtri  14362  blvalps  14373  blval  14374  xblss2  14390  blhalf  14393  comet  14484  xmetxp  14492  txmetcnp  14503  cnmet  14515  ioo2bl  14528  limcmpted  14617  limcimolemlt  14618  cnplimclemr  14623  limccnp2cntop  14631  reldvg  14633  dvfvalap  14635  dvidlemap  14645  dvconst  14646  dvcnp2cntop  14648  dvaddxxbr  14650  dvmulxxbr  14651  dvcoapbr  14656  dvcjbr  14657  dvexp  14660  dvrecap  14662  dvmptcmulcn  14668  dveflem  14672  sin0pilem1  14687  sinperlem  14714  ptolemy  14730  tangtx  14744  abssinper  14752  reexplog  14777  relogexp  14778  cxprec  14816  rpdivcxp  14817  cxpmul  14818  rpabscxpbnd  14844  rplogbval  14848  rplogbreexp  14856  rprelogbmul  14858  logbrec  14863  logbgcd1irraplemap  14872  binom4  14882  wilthlem1  14883  lgslem1  14887  lgslem4  14890  lgsval  14891  lgsfvalg  14892  lgsval2lem  14897  lgsval4lem  14898  lgsvalmod  14906  lgsneg  14911  lgsneg1  14912  lgsmod  14913  lgsdilem  14914  lgsdir2lem4  14918  lgsdir2  14920  lgsdirprm  14921  lgsdir  14922  lgsne0  14925  lgssq  14927  lgssq2  14928  lgsmulsqcoprm  14933  lgsdirnn0  14934  lgsdinn0  14935  lgseisenlem1  14936  lgseisenlem2  14937  m1lgs  14938  2lgsoddprmlem1  14939  2lgsoddprmlem2  14940  2lgsoddprmlem3  14945  2sqlem1  14947  2sqlem2  14948  mul2sq  14949  2sqlem3  14950  2sqlem4  14951  2sqlem8  14956  2sqlem9  14957  2sqlem10  14958  trilpolemeq1  15276  trilpolemlt1  15277  trirec0xor  15281  apdifflemf  15282  apdiff  15284