Theorem oveq1d 6036

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 6028	. 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 1397  (class class class)co 6021

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6024

This theorem is referenced by:  fvoveq1d  6043  csbov2g  6063  caovassg  6184  caovdig  6200  caovdirg  6203  caov12d  6207  caov31d  6208  caov411d  6211  caofinvl  6264  omsuc  6643  nnmsucr  6659  nnm1  6696  nnm2  6697  ecovass  6816  ecoviass  6817  ecovdi  6818  ecovidi  6819  isacnm  7421  addasspig  7553  mulasspig  7555  mulpipq2  7594  distrnqg  7610  ltsonq  7621  ltanqg  7623  ltmnqg  7624  ltexnqq  7631  archnqq  7640  prarloclemarch2  7642  enq0sym  7655  addnq0mo  7670  mulnq0mo  7671  addnnnq0  7672  nqpnq0nq  7676  nq0m0r  7679  nq0a0  7680  nnanq0  7681  distrnq0  7682  addassnq0  7685  addpinq1  7687  prarloclemlo  7717  prarloclem3  7720  prarloclem5  7723  prarloclemcalc  7725  addnqprllem  7750  addnqprulem  7751  appdivnq  7786  recexprlem1ssl  7856  recexprlem1ssu  7857  ltmprr  7865  cauappcvgprlemladdru  7879  cauappcvgprlem1  7882  caucvgprlemnkj  7889  caucvgprlemnbj  7890  caucvgprlemcl  7899  caucvgprlemladdfu  7900  caucvgprlemladdrl  7901  caucvgprlem1  7902  caucvgprprlemcbv  7910  caucvgprprlemval  7911  caucvgprprlemexb  7930  caucvgprprlem1  7932  addcmpblnr  7962  mulcmpblnrlemg  7963  addsrmo  7966  mulsrmo  7967  addsrpr  7968  mulsrpr  7969  ltsrprg  7970  1idsr  7991  pn0sr  7994  recexgt0sr  7996  mulgt0sr  8001  srpospr  8006  prsradd  8009  caucvgsrlemfv  8014  caucvgsrlemcau  8016  caucvgsrlemgt1  8018  caucvgsrlemoffval  8019  caucvgsrlemoffcau  8021  caucvgsrlemoffres  8023  caucvgsrlembnd  8024  caucvgsr  8025  map2psrprg  8028  pitonnlem1p1  8069  pitonnlem2  8070  pitonn  8071  recidpirqlemcalc  8080  ax1rid  8100  axrnegex  8102  axcnre  8104  recriota  8113  nntopi  8117  axcaucvglemval  8120  axcaucvglemcau  8121  axcaucvglemres  8122  mul12  8311  mul4  8314  muladd11  8315  readdcan  8322  muladd11r  8338  add12  8340  cnegex  8360  addcan  8362  negeu  8373  pncan2  8389  addsubass  8392  addsub  8393  2addsub  8396  addsubeq4  8397  subid  8401  subid1  8402  npncan  8403  nppcan  8404  nnpcan  8405  nnncan1  8418  npncan3  8420  pnpcan  8421  pnncan  8423  ppncan  8424  addsub4  8425  negsub  8430  subneg  8431  subeqxfrd  8545  mvlraddd  8546  mvlladdd  8547  mvrraddd  8548  subaddeqd  8551  ine0  8576  mulneg1  8577  ltadd2  8602  apreap  8770  cru  8785  recexap  8836  mulcanapd  8844  div23ap  8874  div13ap  8876  divmulassap  8878  divmulasscomap  8879  divcanap4  8882  muldivdirap  8890  divsubdirap  8891  divmuldivap  8895  divdivdivap  8896  divcanap5  8897  divmul13ap  8898  divmuleqap  8900  divdiv32ap  8903  divcanap7  8904  dmdcanap  8905  divdivap1  8906  divdivap2  8907  divadddivap  8910  divsubdivap  8911  conjmulap  8912  divneg2ap  8919  subrecap  9022  mvllmulapd  9025  lt2mul2div  9062  nndivtr  9188  2halves  9376  halfaddsub  9381  subhalfhalf  9382  avgle1  9388  avgle2  9389  div4p1lem1div2  9401  un0addcl  9438  un0mulcl  9439  peano2z  9518  zneo  9584  nneoor  9585  nneo  9586  zeo  9588  zeo2  9589  deceq1  9618  qreccl  9879  xaddcom  10099  xnegdi  10106  xaddass  10107  xaddass2  10108  xpncan  10109  xleadd1a  10111  xltadd1  10114  xposdif  10120  xadd4d  10123  lincmb01cmp  10241  iccf1o  10242  fz0to4untppr  10362  fzo0addel  10437  fzosubel3  10445  qavgle  10522  2tnp1ge0ge0  10565  fldiv4p1lem1div2  10569  fldiv4lem1div2  10571  ceilqm1lt  10578  flqdiv  10587  modqlt  10599  modqdiffl  10601  modqcyc2  10626  modqaddabs  10628  mulqaddmodid  10630  mulp1mod1  10631  modqmuladd  10632  modqmuladdnn0  10634  qnegmod  10635  addmodid  10638  addmodidr  10639  modqadd2mod  10640  modqm1p1mod0  10641  modqmul12d  10644  modqnegd  10645  modqadd12d  10646  modqsub12d  10647  q2submod  10651  modqmulmodr  10656  modqaddmulmod  10657  modqsubdir  10659  modfzo0difsn  10661  modsumfzodifsn  10662  addmodlteq  10664  frecuzrdgsuc  10680  frecfzennn  10692  iseqovex  10724  seq3-1p  10756  seq3caopr2  10759  seqcaopr2g  10760  seq3caopr  10761  seqcaoprg  10762  seqf1oglem2a  10784  seqf1oglem1  10785  seqf1oglem2  10786  seq3id  10791  seq3homo  10793  seq3z  10794  seqhomog  10796  seqfeq4g  10797  expp1  10812  exprecap  10846  expaddzaplem  10848  expmulzap  10851  expdivap  10856  sqval  10863  sqsubswap  10865  sqdividap  10870  subsq  10912  subsq2  10913  binom2  10917  binom2sub  10919  mulbinom2  10922  binom3  10923  zesq  10924  bernneq2  10927  modqexp  10932  sqoddm1div8  10959  mulsubdivbinom2ap  10977  nn0opthlem1d  10986  nn0opthd  10988  nn0opth2d  10989  facp1  10996  facdiv  11004  facndiv  11005  faclbnd  11007  faclbnd2  11008  faclbnd3  11009  bcval  11015  bccmpl  11020  bcm1k  11026  bcp1n  11027  bcp1nk  11028  bcval5  11029  bcp1m1  11031  bcpasc  11032  bcn2m1  11035  hashprg  11076  hashdifpr  11088  hashfzo  11090  hashfzp1  11092  hashfz0  11093  hashxp  11094  zfz1isolemsplit  11106  zfz1isolem1  11108  seq3coll  11110  lswwrd  11167  ccatfvalfi  11176  ccatass  11192  lswccatn0lsw  11195  wrdlenccats1lenm1g  11220  ccatw2s1leng  11222  ccatswrd  11258  ccatpfx  11289  swrdpfx  11295  pfxpfx  11296  ccats1pfxeq  11302  wrdeqs1cat  11308  wrdind  11310  wrd2ind  11311  pfxccatpfx2  11325  pfxccatin12d  11333  cats1catd  11356  cats2catd  11357  s2leng  11377  s3s4d  11391  s2s5d  11392  s5s2d  11393  reval  11430  crre  11438  remim  11441  remul2  11454  immul2  11461  imval2  11475  cjdivap  11490  caucvgre  11562  cvg1nlemcau  11565  cvg1nlemres  11566  resqrexlemp1rp  11587  resqrexlemfp1  11590  resqrexlemover  11591  resqrexlemcalc1  11595  resqrexlemcalc3  11597  resqrexlemnm  11599  resqrexlemoverl  11602  resqrexlemglsq  11603  resqrexlemga  11604  resqrexlemsqa  11605  resqrexlemex  11606  resqrex  11607  sqrtdiv  11623  absvalsq  11634  absreimsq  11648  absdivap  11651  cau3lem  11695  maxabslemlub  11788  maxabslemval  11789  max0addsup  11800  minabs  11817  bdtrilem  11820  bdtri  11821  xrmaxaddlem  11841  xrmaxadd  11842  xrbdtri  11857  clim  11862  clim2  11864  climshftlemg  11883  climshft2  11887  climcn1  11889  climcn2  11890  subcn2  11892  reccn2ap  11894  climmulc2  11912  climsubc2  11914  clim2ser  11918  iser3shft  11927  climcau  11928  serf0  11933  fzosump1  11999  fsum1p  12000  fsump1  12002  sumsplitdc  12014  fsump1i  12015  mptfzshft  12024  fisum0diag2  12029  fsumconst  12036  fsumdifsnconst  12037  modfsummodlemstep  12039  modfsummod  12040  telfsumo  12048  fsumparts  12052  fsumrelem  12053  hash2iun1dif1  12062  binomlem  12065  binom  12066  binom1p  12067  binom1dif  12069  bcxmas  12071  isumsplit  12073  isum1p  12074  arisum  12080  arisum2  12081  trireciplem  12082  geoserap  12089  geolim  12093  geolim2  12094  georeclim  12095  geo2sum  12096  geoisum1  12101  cvgratnnlemseq  12108  cvgratnnlemsumlt  12110  cvgratnnlemfm  12111  cvgratz  12114  mertenslemi1  12117  mertenslem2  12118  mertensabs  12119  fprod1p  12181  fprodp1  12182  fprodcl2lem  12187  fprodfac  12197  fprodeq0  12199  fprodconst  12202  fprodrec  12211  fprodsplit1f  12216  fprodmodd  12223  efcllemp  12240  ef0lem  12242  efval  12243  esum  12244  ege2le3  12253  efaddlem  12256  efsep  12273  effsumlt  12274  eft0val  12275  efgt1p2  12277  efgt1p  12278  sinval  12284  cosval  12285  resinval  12297  recosval  12298  efi4p  12299  resin4p  12300  recos4p  12301  sinneg  12308  cosneg  12309  efival  12314  sinadd  12318  cosadd  12319  tanaddap  12321  sinmul  12326  cosmul  12327  cos2t  12332  cos2tsin  12333  ef01bndlem  12338  absefib  12353  demoivre  12355  demoivreALT  12356  eirraplem  12359  p1modz1  12376  dvdsmodexp  12377  moddvds  12381  mulmoddvds  12445  3dvds2dec  12448  zeo3  12450  odd2np1lem  12454  odd2np1  12455  oexpneg  12459  2tp1odd  12466  ltoddhalfle  12475  opoe  12477  opeo  12479  omeo  12480  m1expo  12482  m1exp1  12483  nn0o1gt2  12487  nn0o  12489  divalglemnn  12500  divalglemqt  12501  divalglemeunn  12503  divalglemex  12504  divalglemeuneg  12505  flodddiv4  12518  flodddiv4t2lthalf  12521  bitsp1o  12535  bitsmod  12538  bitsinv1lem  12543  gcdaddm  12576  bezoutlemnewy  12588  bezoutlema  12591  bezoutlemb  12592  bezoutlemex  12593  bezoutlemaz  12595  mulgcd  12608  gcddiv  12611  gcdmultiplez  12613  rpmulgcd  12618  rplpwr  12619  uzwodc  12629  lcmgcdlem  12670  lcmgcd  12671  divgcdcoprmex  12695  cncongr2  12697  prmexpb  12744  rpexp  12746  rpexp1i  12747  sqrt2irrlem  12754  oddpwdclemxy  12762  oddpwdclemndvds  12764  sqpweven  12768  2sqpwodd  12769  sqne2sq  12770  qmuldeneqnum  12788  nn0gcdsq  12793  zgcdsq  12794  numdensq  12795  dfphi2  12813  phiprmpw  12815  phiprm  12816  eulerthlema  12823  eulerthlemh  12824  eulerthlemth  12825  fermltl  12827  prmdiv  12828  prmdiveq  12829  prmdivdiv  12830  hashgcdlem  12831  odzval  12835  odzcllem  12836  odzdvds  12839  vfermltl  12845  powm2modprm  12846  reumodprminv  12847  modprm0  12848  nnnn0modprm0  12849  modprmn0modprm0  12850  coprimeprodsq  12851  coprimeprodsq2  12852  pythagtriplem1  12859  pythagtriplem3  12861  pythagtriplem4  12862  pythagtriplem6  12864  pythagtriplem7  12865  pythagtriplem12  12869  pythagtriplem14  12871  pythagtriplem15  12872  pythagtriplem16  12873  pythagtriplem17  12874  pythagtriplem18  12875  pceu  12889  pczpre  12891  pcdiv  12896  pcqdiv  12901  pcrec  12902  pczndvds  12910  pcneg  12919  pc2dvds  12924  pcprmpw2  12927  pcaddlem  12933  pcadd  12934  fldivp1  12942  pockthlem  12950  pockthi  12952  4sqlem5  12976  4sqlem9  12980  4sqlem10  12981  4sqlem2  12983  4sqlem3  12984  4sqlem4  12986  mul4sqlem  12987  4sqlem11  12995  4sqlem12  12996  4sqlem14  12998  4sqlem15  12999  4sqlem17  13001  4sqlem19  13003  ennnfonelemkh  13054  ennnfonelemhf1o  13055  setscomd  13144  ressressg  13179  qusex  13429  qusin  13430  grpinvalem  13489  grpinva  13490  grprida  13491  gsumsplit1r  13502  isnsgrp  13510  sgrpass  13512  sgrp1  13515  sgrppropd  13517  prdssgrpd  13519  mnd12g  13532  mndpropd  13544  prdsidlem  13551  prdsmndd  13552  imasmnd2  13556  mhmex  13566  mhmlin  13571  grprcan  13641  grpinvid1  13656  isgrpinv  13658  grplcan  13666  grpasscan1  13667  grplmulf1o  13678  grpinvadd  13682  grpinvsub  13686  grpsubsub4  13697  grppnpcan2  13698  grpnpncan  13699  dfgrp3mlem  13702  dfgrp3m  13703  grplactcnv  13706  prdsinvlem  13712  imasgrp2  13718  mhmlem  13722  mhmid  13723  mhmmnd  13724  mulgnnp1  13738  mulg2  13739  mulgnn0p1  13741  mulgsubcl  13744  mulgneg  13748  mulgaddcomlem  13753  mulgaddcom  13754  mulgz  13758  mulgnn0dir  13760  mulgdirlem  13761  mulgdir  13762  mulgneg2  13764  mulgnnass  13765  mulgnn0ass  13766  mulgass  13767  mulgassr  13768  mulgmodid  13769  mulgsubdir  13770  submmulg  13774  isnsg3  13815  nmzsubg  13818  ssnmz  13819  0nsg  13822  eqger  13832  eqgid  13834  eqgcpbl  13836  ghmlin  13856  ghmmulg  13864  ghmnsgima  13876  ghmnsgpreima  13877  conjghm  13884  conjnmz  13887  ablsub2inv  13919  abladdsub4  13922  abladdsub  13923  ablpncan2  13924  ablpnpcan  13928  ablnncan  13929  ablnnncan1  13932  gsumfzconst  13949  gsumfzsnfd  13953  gsumsplit0  13954  mgpress  13966  rngass  13974  rngdi  13975  rngdir  13976  rnglz  13980  rngmneg1  13982  rngsubdir  13987  rngpropd  13990  imasrng  13991  srgass  14006  srgmulgass  14024  srgpcomp  14025  srgpcompp  14026  srgpcomppsc  14027  ringpropd  14073  ringlz  14078  ring1eq0  14083  ringnegl  14086  ringmneg1  14088  ringsubdir  14092  mulgass2  14093  ring1  14094  imasring  14099  opprrng  14112  opprring  14114  unitgrp  14152  dvrcan1  14176  rdivmuldivd  14180  subrginv  14273  resrhm  14284  unitrrg  14303  islmod  14327  lmodlema  14328  islmodd  14329  lmod0vs  14357  lmodvs0  14358  lmodvsmmulgdi  14359  lmodvneg1  14366  lmodvsneg  14367  lmodsubvs  14379  lmodsubdi  14380  lmodsubdir  14381  lmodprop2d  14384  rmodislmodlem  14386  rmodislmod  14387  lsssetm  14392  islssmd  14395  lssclg  14400  lssvacl  14401  lss1d  14419  lsspropdg  14467  sraval  14473  rnglidlmcl  14516  gsumfzfsumlemm  14623  znunit  14695  mplsubgfilemcl  14740  resttop  14921  restco  14925  restin  14927  lmfval  14944  cnprcl2k  14957  txrest  15027  txdis1cn  15029  cnmpt2res  15048  psmettri2  15079  psmettri  15081  xmettri2  15112  xmettri  15123  mettri  15124  metrtri  15128  blvalps  15139  blval  15140  xblss2  15156  blhalf  15159  comet  15250  xmetxp  15258  txmetcnp  15269  cnmet  15281  ioo2bl  15302  ivthreinc  15396  limcmpted  15414  limcimolemlt  15415  cnplimclemr  15420  limccnp2cntop  15428  reldvg  15430  dvfvalap  15432  dvidlemap  15442  dvidrelem  15443  dvidsslem  15444  dvconst  15445  dvconstre  15447  dvconstss  15449  dvcnp2cntop  15450  dvaddxxbr  15452  dvmulxxbr  15453  dvcoapbr  15458  dvcjbr  15459  dvexp  15462  dvrecap  15464  dvmptcmulcn  15472  dveflem  15477  plyval  15483  elply2  15486  elplyr  15491  elplyd  15492  ply1termlem  15493  plyaddlem1  15498  plymullem1  15499  plycoeid3  15508  plycjlemc  15511  dvply1  15516  sin0pilem1  15532  sinperlem  15559  ptolemy  15575  tangtx  15589  abssinper  15597  reexplog  15622  relogexp  15623  cxprec  15661  rpdivcxp  15662  cxpmul  15663  rpabscxpbnd  15691  rplogbval  15696  rplogbreexp  15704  rprelogbmul  15706  logbrec  15711  logbgcd1irraplemap  15720  binom4  15730  wilthlem1  15731  mpodvdsmulf1o  15741  sgmppw  15743  0sgmppw  15744  1sgmprm  15745  1sgm2ppw  15746  perfectlem1  15750  perfectlem2  15751  perfect  15752  lgslem1  15756  lgslem4  15759  lgsval  15760  lgsfvalg  15761  lgsval2lem  15766  lgsval4lem  15767  lgsvalmod  15775  lgsneg  15780  lgsneg1  15781  lgsmod  15782  lgsdilem  15783  lgsdir2lem4  15787  lgsdir2  15789  lgsdirprm  15790  lgsdir  15791  lgsne0  15794  lgssq  15796  lgssq2  15797  lgsmulsqcoprm  15802  lgsdirnn0  15803  lgsdinn0  15804  gausslemma2dlem1a  15814  gausslemma2dlem4  15820  gausslemma2dlem5a  15821  gausslemma2dlem5  15822  gausslemma2dlem6  15823  gausslemma2dlem7  15824  gausslemma2d  15825  lgseisenlem1  15826  lgseisenlem2  15827  lgseisenlem3  15828  lgseisenlem4  15829  lgseisen  15830  lgsquadlem1  15833  lgsquadlem2  15834  lgsquad2lem1  15837  lgsquad2lem2  15838  lgsquad3  15840  m1lgs  15841  2lgslem1a  15844  2lgslem1c  15846  2lgslem3a  15849  2lgslem3b  15850  2lgslem3c  15851  2lgslem3d  15852  2lgslem3a1  15853  2lgslem3b1  15854  2lgslem3c1  15855  2lgslem3d1  15856  2lgsoddprmlem1  15861  2lgsoddprmlem2  15862  2lgsoddprmlem3  15867  2sqlem1  15870  2sqlem2  15871  mul2sq  15872  2sqlem3  15873  2sqlem4  15874  2sqlem8  15879  2sqlem9  15880  2sqlem10  15881  vdegp1bid  16193  uspgr2wlkeqi  16245  isclwwlk  16272  clwwlkccatlem  16278  clwwlknonex2  16317  trilpolemeq1  16703  trilpolemlt1  16704  trirec0xor  16708  apdifflemf  16709  apdiff  16711  qdiff  16712  gsumgfsumlem  16743  gsumgfsum  16744