Theorem oveq1d 6056

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 6048	. 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 1398  (class class class)co 6041

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-br 4103  df-iota 5303  df-fv 5351  df-ov 6044

This theorem is referenced by:  fvoveq1d  6063  csbov2g  6083  caovassg  6204  caovdig  6220  caovdirg  6223  caov12d  6227  caov31d  6228  caov411d  6231  caofinvl  6283  suppofss1dcl  6455  suppofss2dcl  6456  omsuc  6696  nnmsucr  6712  nnm1  6749  nnm2  6750  ecovass  6869  ecoviass  6870  ecovdi  6871  ecovidi  6872  isacnm  7501  addasspig  7633  mulasspig  7635  mulpipq2  7674  distrnqg  7690  ltsonq  7701  ltanqg  7703  ltmnqg  7704  ltexnqq  7711  archnqq  7720  prarloclemarch2  7722  enq0sym  7735  addnq0mo  7750  mulnq0mo  7751  addnnnq0  7752  nqpnq0nq  7756  nq0m0r  7759  nq0a0  7760  nnanq0  7761  distrnq0  7762  addassnq0  7765  addpinq1  7767  prarloclemlo  7797  prarloclem3  7800  prarloclem5  7803  prarloclemcalc  7805  addnqprllem  7830  addnqprulem  7831  appdivnq  7866  recexprlem1ssl  7936  recexprlem1ssu  7937  ltmprr  7945  cauappcvgprlemladdru  7959  cauappcvgprlem1  7962  caucvgprlemnkj  7969  caucvgprlemnbj  7970  caucvgprlemcl  7979  caucvgprlemladdfu  7980  caucvgprlemladdrl  7981  caucvgprlem1  7982  caucvgprprlemcbv  7990  caucvgprprlemval  7991  caucvgprprlemexb  8010  caucvgprprlem1  8012  addcmpblnr  8042  mulcmpblnrlemg  8043  addsrmo  8046  mulsrmo  8047  addsrpr  8048  mulsrpr  8049  ltsrprg  8050  1idsr  8071  pn0sr  8074  recexgt0sr  8076  mulgt0sr  8081  srpospr  8086  prsradd  8089  caucvgsrlemfv  8094  caucvgsrlemcau  8096  caucvgsrlemgt1  8098  caucvgsrlemoffval  8099  caucvgsrlemoffcau  8101  caucvgsrlemoffres  8103  caucvgsrlembnd  8104  caucvgsr  8105  map2psrprg  8108  pitonnlem1p1  8149  pitonnlem2  8150  pitonn  8151  recidpirqlemcalc  8160  ax1rid  8180  axrnegex  8182  axcnre  8184  recriota  8193  nntopi  8197  axcaucvglemval  8200  axcaucvglemcau  8201  axcaucvglemres  8202  mul12  8390  mul4  8393  muladd11  8394  readdcan  8401  muladd11r  8417  add12  8419  cnegex  8439  addcan  8441  negeu  8452  pncan2  8468  addsubass  8471  addsub  8472  2addsub  8475  addsubeq4  8476  subid  8480  subid1  8481  npncan  8482  nppcan  8483  nnpcan  8484  nnncan1  8497  npncan3  8499  pnpcan  8500  pnncan  8502  ppncan  8503  addsub4  8504  negsub  8509  subneg  8510  subeqxfrd  8624  mvlraddd  8625  mvlladdd  8626  mvrraddd  8627  subaddeqd  8630  ine0  8655  mulneg1  8656  ltadd2  8681  apreap  8849  cru  8864  recexap  8915  mulcanapd  8923  div23ap  8953  div13ap  8955  divmulassap  8957  divmulasscomap  8958  divcanap4  8961  muldivdirap  8969  divsubdirap  8970  divmuldivap  8974  divdivdivap  8975  divcanap5  8976  divmul13ap  8977  divmuleqap  8979  divdiv32ap  8982  divcanap7  8983  dmdcanap  8984  divdivap1  8985  divdivap2  8986  divadddivap  8989  divsubdivap  8990  conjmulap  8991  divneg2ap  8998  subrecap  9101  mvllmulapd  9104  lt2mul2div  9141  nndivtr  9267  2halves  9455  halfaddsub  9460  subhalfhalf  9461  avgle1  9467  avgle2  9468  div4p1lem1div2  9480  un0addcl  9517  un0mulcl  9518  peano2z  9599  zneo  9665  nneoor  9666  nneo  9667  zeo  9669  zeo2  9670  deceq1  9699  qreccl  9960  xaddcom  10180  xnegdi  10187  xaddass  10188  xaddass2  10189  xpncan  10190  xleadd1a  10192  xltadd1  10195  xposdif  10201  xadd4d  10204  lincmb01cmp  10322  lincmble  10323  iccf1o  10324  fz0to4untppr  10444  fzo0addel  10519  fzosubel3  10527  qavgle  10604  2tnp1ge0ge0  10647  fldiv4p1lem1div2  10651  fldiv4lem1div2  10653  ceilqm1lt  10660  flqdiv  10669  modqlt  10681  modqdiffl  10683  modqcyc2  10708  modqaddabs  10710  mulqaddmodid  10712  mulp1mod1  10713  modqmuladd  10714  modqmuladdnn0  10716  qnegmod  10717  addmodid  10720  addmodidr  10721  modqadd2mod  10722  modqm1p1mod0  10723  modqmul12d  10726  modqnegd  10727  modqadd12d  10728  modqsub12d  10729  q2submod  10733  modqmulmodr  10738  modqaddmulmod  10739  modqsubdir  10741  modfzo0difsn  10743  modsumfzodifsn  10744  addmodlteq  10746  frecuzrdgsuc  10762  frecfzennn  10774  iseqovex  10806  seq3-1p  10838  seq3caopr2  10841  seqcaopr2g  10842  seq3caopr  10843  seqcaoprg  10844  seqf1oglem2a  10866  seqf1oglem1  10867  seqf1oglem2  10868  seq3id  10873  seq3homo  10875  seq3z  10876  seqhomog  10878  seqfeq4g  10879  expp1  10894  exprecap  10928  expaddzaplem  10930  expmulzap  10933  expdivap  10938  sqval  10945  sqsubswap  10947  sqdividap  10952  subsq  10994  subsq2  10995  binom2  10999  binom2sub  11001  mulbinom2  11004  binom3  11005  zesq  11006  bernneq2  11009  modqexp  11014  sqoddm1div8  11041  mulsubdivbinom2ap  11059  nn0opthlem1d  11068  nn0opthd  11070  nn0opth2d  11071  facp1  11078  facdiv  11086  facndiv  11087  faclbnd  11089  faclbnd2  11090  faclbnd3  11091  bcval  11097  bccmpl  11102  bcm1k  11108  bcp1n  11109  bcp1nk  11110  bcval5  11111  bcp1m1  11113  bcpasc  11114  bcn2m1  11117  hashprg  11158  hashdifpr  11170  hashfzo  11172  hashfzp1  11174  hashfz0  11175  hashxp  11176  zfz1isolemsplit  11188  zfz1isolem1  11190  seq3coll  11192  lswwrd  11249  ccatfvalfi  11258  ccatass  11274  lswccatn0lsw  11277  wrdlenccats1lenm1g  11302  ccatw2s1leng  11304  ccatswrd  11340  ccatpfx  11371  swrdpfx  11377  pfxpfx  11378  ccats1pfxeq  11384  wrdeqs1cat  11390  wrdind  11392  wrd2ind  11393  pfxccatpfx2  11407  pfxccatin12d  11415  cats1catd  11438  cats2catd  11439  s2leng  11459  s3s4d  11473  s2s5d  11474  s5s2d  11475  reval  11512  crre  11520  remim  11523  remul2  11536  immul2  11543  imval2  11557  cjdivap  11572  caucvgre  11644  cvg1nlemcau  11647  cvg1nlemres  11648  resqrexlemp1rp  11669  resqrexlemfp1  11672  resqrexlemover  11673  resqrexlemcalc1  11677  resqrexlemcalc3  11679  resqrexlemnm  11681  resqrexlemoverl  11684  resqrexlemglsq  11685  resqrexlemga  11686  resqrexlemsqa  11687  resqrexlemex  11688  resqrex  11689  sqrtdiv  11705  absvalsq  11716  absreimsq  11730  absdivap  11733  cau3lem  11777  maxabslemlub  11870  maxabslemval  11871  max0addsup  11882  minabs  11899  bdtrilem  11902  bdtri  11903  xrmaxaddlem  11923  xrmaxadd  11924  xrbdtri  11939  clim  11944  clim2  11946  climshftlemg  11965  climshft2  11969  climcn1  11971  climcn2  11972  subcn2  11974  reccn2ap  11976  climmulc2  11994  climsubc2  11996  clim2ser  12000  iser3shft  12009  climcau  12010  serf0  12015  fzosump1  12081  fsum1p  12082  fsump1  12084  sumsplitdc  12096  fsump1i  12097  mptfzshft  12106  fisum0diag2  12111  fsumconst  12118  fsumdifsnconst  12119  modfsummodlemstep  12121  modfsummod  12122  telfsumo  12130  fsumparts  12134  fsumrelem  12135  hash2iun1dif1  12144  binomlem  12147  binom  12148  binom1p  12149  binom1dif  12151  bcxmas  12153  isumsplit  12155  isum1p  12156  arisum  12162  arisum2  12163  trireciplem  12164  geoserap  12171  geolim  12175  geolim2  12176  georeclim  12177  geo2sum  12178  geoisum1  12183  cvgratnnlemseq  12190  cvgratnnlemsumlt  12192  cvgratnnlemfm  12193  cvgratz  12196  mertenslemi1  12199  mertenslem2  12200  mertensabs  12201  fprod1p  12263  fprodp1  12264  fprodcl2lem  12269  fprodfac  12279  fprodeq0  12281  fprodconst  12284  fprodrec  12293  fprodsplit1f  12298  fprodmodd  12305  efcllemp  12322  ef0lem  12324  efval  12325  esum  12326  ege2le3  12335  efaddlem  12338  efsep  12355  effsumlt  12356  eft0val  12357  efgt1p2  12359  efgt1p  12360  sinval  12366  cosval  12367  resinval  12379  recosval  12380  efi4p  12381  resin4p  12382  recos4p  12383  sinneg  12390  cosneg  12391  efival  12396  sinadd  12400  cosadd  12401  tanaddap  12403  sinmul  12408  cosmul  12409  cos2t  12414  cos2tsin  12415  ef01bndlem  12420  absefib  12435  demoivre  12437  demoivreALT  12438  eirraplem  12441  p1modz1  12458  dvdsmodexp  12459  moddvds  12463  mulmoddvds  12527  3dvds2dec  12530  zeo3  12532  odd2np1lem  12536  odd2np1  12537  oexpneg  12541  2tp1odd  12548  ltoddhalfle  12557  opoe  12559  opeo  12561  omeo  12562  m1expo  12564  m1exp1  12565  nn0o1gt2  12569  nn0o  12571  divalglemnn  12582  divalglemqt  12583  divalglemeunn  12585  divalglemex  12586  divalglemeuneg  12587  flodddiv4  12600  flodddiv4t2lthalf  12603  bitsp1o  12617  bitsmod  12620  bitsinv1lem  12625  gcdaddm  12658  bezoutlemnewy  12670  bezoutlema  12673  bezoutlemb  12674  bezoutlemex  12675  bezoutlemaz  12677  mulgcd  12690  gcddiv  12693  gcdmultiplez  12695  rpmulgcd  12700  rplpwr  12701  uzwodc  12711  lcmgcdlem  12752  lcmgcd  12753  divgcdcoprmex  12777  cncongr2  12779  prmexpb  12826  rpexp  12828  rpexp1i  12829  sqrt2irrlem  12836  oddpwdclemxy  12844  oddpwdclemndvds  12846  sqpweven  12850  2sqpwodd  12851  sqne2sq  12852  qmuldeneqnum  12870  nn0gcdsq  12875  zgcdsq  12876  numdensq  12877  dfphi2  12895  phiprmpw  12897  phiprm  12898  eulerthlema  12905  eulerthlemh  12906  eulerthlemth  12907  fermltl  12909  prmdiv  12910  prmdiveq  12911  prmdivdiv  12912  hashgcdlem  12913  odzval  12917  odzcllem  12918  odzdvds  12921  vfermltl  12927  powm2modprm  12928  reumodprminv  12929  modprm0  12930  nnnn0modprm0  12931  modprmn0modprm0  12932  coprimeprodsq  12933  coprimeprodsq2  12934  pythagtriplem1  12941  pythagtriplem3  12943  pythagtriplem4  12944  pythagtriplem6  12946  pythagtriplem7  12947  pythagtriplem12  12951  pythagtriplem14  12953  pythagtriplem15  12954  pythagtriplem16  12955  pythagtriplem17  12956  pythagtriplem18  12957  pceu  12971  pczpre  12973  pcdiv  12978  pcqdiv  12983  pcrec  12984  pczndvds  12992  pcneg  13001  pc2dvds  13006  pcprmpw2  13009  pcaddlem  13015  pcadd  13016  fldivp1  13024  pockthlem  13032  pockthi  13034  4sqlem5  13058  4sqlem9  13062  4sqlem10  13063  4sqlem2  13065  4sqlem3  13066  4sqlem4  13068  mul4sqlem  13069  4sqlem11  13077  4sqlem12  13078  4sqlem14  13080  4sqlem15  13081  4sqlem17  13083  4sqlem19  13085  ennnfonelemkh  13137  ennnfonelemhf1o  13138  setscomd  13227  ressressg  13262  qusex  13512  qusin  13513  grpinvalem  13572  grpinva  13573  grprida  13574  gsumsplit1r  13585  isnsgrp  13593  sgrpass  13595  sgrp1  13598  sgrppropd  13600  prdssgrpd  13602  mnd12g  13615  mndpropd  13627  prdsidlem  13634  prdsmndd  13635  imasmnd2  13639  mhmex  13649  mhmlin  13654  grprcan  13724  grpinvid1  13739  isgrpinv  13741  grplcan  13749  grpasscan1  13750  grplmulf1o  13761  grpinvadd  13765  grpinvsub  13769  grpsubsub4  13780  grppnpcan2  13781  grpnpncan  13782  dfgrp3mlem  13785  dfgrp3m  13786  grplactcnv  13789  prdsinvlem  13795  imasgrp2  13801  mhmlem  13805  mhmid  13806  mhmmnd  13807  mulgnnp1  13821  mulg2  13822  mulgnn0p1  13824  mulgsubcl  13827  mulgneg  13831  mulgaddcomlem  13836  mulgaddcom  13837  mulgz  13841  mulgnn0dir  13843  mulgdirlem  13844  mulgdir  13845  mulgneg2  13847  mulgnnass  13848  mulgnn0ass  13849  mulgass  13850  mulgassr  13851  mulgmodid  13852  mulgsubdir  13853  submmulg  13857  isnsg3  13898  nmzsubg  13901  ssnmz  13902  0nsg  13905  eqger  13915  eqgid  13917  eqgcpbl  13919  ghmlin  13939  ghmmulg  13947  ghmnsgima  13959  ghmnsgpreima  13960  conjghm  13967  conjnmz  13970  ablsub2inv  14002  abladdsub4  14005  abladdsub  14006  ablpncan2  14007  ablpnpcan  14011  ablnncan  14012  ablnnncan1  14015  gsumfzconst  14032  gsumfzsnfd  14036  gsumsplit0  14037  mgpress  14049  rngass  14057  rngdi  14058  rngdir  14059  rnglz  14063  rngmneg1  14065  rngsubdir  14070  rngpropd  14073  imasrng  14074  srgass  14089  srgmulgass  14107  srgpcomp  14108  srgpcompp  14109  srgpcomppsc  14110  ringpropd  14156  ringlz  14161  ring1eq0  14166  ringnegl  14169  ringmneg1  14171  ringsubdir  14175  mulgass2  14176  ring1  14177  imasring  14182  opprrng  14195  opprring  14197  unitgrp  14235  dvrcan1  14259  rdivmuldivd  14263  subrginv  14356  resrhm  14367  unitrrg  14387  islmod  14411  lmodlema  14412  islmodd  14413  lmod0vs  14441  lmodvs0  14442  lmodvsmmulgdi  14443  lmodvneg1  14450  lmodvsneg  14451  lmodsubvs  14463  lmodsubdi  14464  lmodsubdir  14465  lmodprop2d  14468  rmodislmodlem  14470  rmodislmod  14471  lsssetm  14476  islssmd  14479  lssclg  14484  lssvacl  14485  lss1d  14503  lsspropdg  14551  sraval  14557  rnglidlmcl  14600  gsumfzfsumlemm  14707  znunit  14779  mplsubgfilemcl  14824  resttop  15005  restco  15009  restin  15011  lmfval  15028  cnprcl2k  15041  txrest  15111  txdis1cn  15113  cnmpt2res  15132  psmettri2  15163  psmettri  15165  xmettri2  15196  xmettri  15207  mettri  15208  metrtri  15212  blvalps  15223  blval  15224  xblss2  15240  blhalf  15243  comet  15334  xmetxp  15342  txmetcnp  15353  cnmet  15365  ioo2bl  15386  ivthreinc  15480  limcmpted  15498  limcimolemlt  15499  cnplimclemr  15504  limccnp2cntop  15512  reldvg  15514  dvfvalap  15516  dvidlemap  15526  dvidrelem  15527  dvidsslem  15528  dvconst  15529  dvconstre  15531  dvconstss  15533  dvcnp2cntop  15534  dvaddxxbr  15536  dvmulxxbr  15537  dvcoapbr  15542  dvcjbr  15543  dvexp  15546  dvrecap  15548  dvmptcmulcn  15556  dveflem  15561  plyval  15567  elply2  15570  elplyr  15575  elplyd  15576  ply1termlem  15577  plyaddlem1  15582  plymullem1  15583  plycoeid3  15592  plycjlemc  15595  dvply1  15600  sin0pilem1  15616  sinperlem  15643  ptolemy  15659  tangtx  15673  abssinper  15681  reexplog  15706  relogexp  15707  cxprec  15745  rpdivcxp  15746  cxpmul  15747  rpabscxpbnd  15775  rplogbval  15780  rplogbreexp  15788  rprelogbmul  15790  logbrec  15795  logbgcd1irraplemap  15804  binom4  15814  pellexlem2  15816  pellexlem3  15817  wilthlem1  15818  mpodvdsmulf1o  15828  sgmppw  15830  0sgmppw  15831  1sgmprm  15832  1sgm2ppw  15833  perfectlem1  15837  perfectlem2  15838  perfect  15839  lgslem1  15843  lgslem4  15846  lgsval  15847  lgsfvalg  15848  lgsval2lem  15853  lgsval4lem  15854  lgsvalmod  15862  lgsneg  15867  lgsneg1  15868  lgsmod  15869  lgsdilem  15870  lgsdir2lem4  15874  lgsdir2  15876  lgsdirprm  15877  lgsdir  15878  lgsne0  15881  lgssq  15883  lgssq2  15884  lgsmulsqcoprm  15889  lgsdirnn0  15890  lgsdinn0  15891  gausslemma2dlem1a  15901  gausslemma2dlem4  15907  gausslemma2dlem5a  15908  gausslemma2dlem5  15909  gausslemma2dlem6  15910  gausslemma2dlem7  15911  gausslemma2d  15912  lgseisenlem1  15913  lgseisenlem2  15914  lgseisenlem3  15915  lgseisenlem4  15916  lgseisen  15917  lgsquadlem1  15920  lgsquadlem2  15921  lgsquad2lem1  15924  lgsquad2lem2  15925  lgsquad3  15927  m1lgs  15928  2lgslem1a  15931  2lgslem1c  15933  2lgslem3a  15936  2lgslem3b  15937  2lgslem3c  15938  2lgslem3d  15939  2lgslem3a1  15940  2lgslem3b1  15941  2lgslem3c1  15942  2lgslem3d1  15943  2lgsoddprmlem1  15948  2lgsoddprmlem2  15949  2lgsoddprmlem3  15954  2sqlem1  15957  2sqlem2  15958  mul2sq  15959  2sqlem3  15960  2sqlem4  15961  2sqlem8  15966  2sqlem9  15967  2sqlem10  15968  vdegp1bid  16280  uspgr2wlkeqi  16332  isclwwlk  16359  clwwlkccatlem  16365  clwwlknonex2  16404  repiecele0  16780  repiecege0  16781  repiecef  16782  trilpolemeq1  16794  trilpolemlt1  16795  trirec0xor  16799  apdifflemf  16800  apdiff  16802  qdiff  16803  gsumgfsumlem  16834  gsumgfsum  16835