Theorem oveq1d 6033

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 6025	. 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 6018

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 6021

This theorem is referenced by:  fvoveq1d  6040  csbov2g  6060  caovassg  6181  caovdig  6197  caovdirg  6200  caov12d  6204  caov31d  6205  caov411d  6208  caofinvl  6261  omsuc  6640  nnmsucr  6656  nnm1  6693  nnm2  6694  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  isacnm  7418  addasspig  7550  mulasspig  7552  mulpipq2  7591  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  archnqq  7637  prarloclemarch2  7639  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  nqpnq0nq  7673  nq0m0r  7676  nq0a0  7677  nnanq0  7678  distrnq0  7679  addassnq0  7682  addpinq1  7684  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prarloclemcalc  7722  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemexb  7927  caucvgprprlem1  7929  addcmpblnr  7959  mulcmpblnrlemg  7960  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  ltsrprg  7967  1idsr  7988  pn0sr  7991  recexgt0sr  7993  mulgt0sr  7998  srpospr  8003  prsradd  8006  caucvgsrlemfv  8011  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsrlembnd  8021  caucvgsr  8022  map2psrprg  8025  pitonnlem1p1  8066  pitonnlem2  8067  pitonn  8068  recidpirqlemcalc  8077  ax1rid  8097  axrnegex  8099  axcnre  8101  recriota  8110  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  mul12  8308  mul4  8311  muladd11  8312  readdcan  8319  muladd11r  8335  add12  8337  cnegex  8357  addcan  8359  negeu  8370  pncan2  8386  addsubass  8389  addsub  8390  2addsub  8393  addsubeq4  8394  subid  8398  subid1  8399  npncan  8400  nppcan  8401  nnpcan  8402  nnncan1  8415  npncan3  8417  pnpcan  8418  pnncan  8420  ppncan  8421  addsub4  8422  negsub  8427  subneg  8428  subeqxfrd  8542  mvlraddd  8543  mvlladdd  8544  mvrraddd  8545  subaddeqd  8548  ine0  8573  mulneg1  8574  ltadd2  8599  apreap  8767  cru  8782  recexap  8833  mulcanapd  8841  div23ap  8871  div13ap  8873  divmulassap  8875  divmulasscomap  8876  divcanap4  8879  muldivdirap  8887  divsubdirap  8888  divmuldivap  8892  divdivdivap  8893  divcanap5  8894  divmul13ap  8895  divmuleqap  8897  divdiv32ap  8900  divcanap7  8901  dmdcanap  8902  divdivap1  8903  divdivap2  8904  divadddivap  8907  divsubdivap  8908  conjmulap  8909  divneg2ap  8916  subrecap  9019  mvllmulapd  9022  lt2mul2div  9059  nndivtr  9185  2halves  9373  halfaddsub  9378  subhalfhalf  9379  avgle1  9385  avgle2  9386  div4p1lem1div2  9398  un0addcl  9435  un0mulcl  9436  peano2z  9515  zneo  9581  nneoor  9582  nneo  9583  zeo  9585  zeo2  9586  deceq1  9615  qreccl  9876  xaddcom  10096  xnegdi  10103  xaddass  10104  xaddass2  10105  xpncan  10106  xleadd1a  10108  xltadd1  10111  xposdif  10117  xadd4d  10120  lincmb01cmp  10238  iccf1o  10239  fz0to4untppr  10359  fzo0addel  10433  fzosubel3  10441  qavgle  10518  2tnp1ge0ge0  10561  fldiv4p1lem1div2  10565  fldiv4lem1div2  10567  ceilqm1lt  10574  flqdiv  10583  modqlt  10595  modqdiffl  10597  modqcyc2  10622  modqaddabs  10624  mulqaddmodid  10626  mulp1mod1  10627  modqmuladd  10628  modqmuladdnn0  10630  qnegmod  10631  addmodid  10634  addmodidr  10635  modqadd2mod  10636  modqm1p1mod0  10637  modqmul12d  10640  modqnegd  10641  modqadd12d  10642  modqsub12d  10643  q2submod  10647  modqmulmodr  10652  modqaddmulmod  10653  modqsubdir  10655  modfzo0difsn  10657  modsumfzodifsn  10658  addmodlteq  10660  frecuzrdgsuc  10676  frecfzennn  10688  iseqovex  10720  seq3-1p  10752  seq3caopr2  10755  seqcaopr2g  10756  seq3caopr  10757  seqcaoprg  10758  seqf1oglem2a  10780  seqf1oglem1  10781  seqf1oglem2  10782  seq3id  10787  seq3homo  10789  seq3z  10790  seqhomog  10792  seqfeq4g  10793  expp1  10808  exprecap  10842  expaddzaplem  10844  expmulzap  10847  expdivap  10852  sqval  10859  sqsubswap  10861  sqdividap  10866  subsq  10908  subsq2  10909  binom2  10913  binom2sub  10915  mulbinom2  10918  binom3  10919  zesq  10920  bernneq2  10923  modqexp  10928  sqoddm1div8  10955  mulsubdivbinom2ap  10973  nn0opthlem1d  10982  nn0opthd  10984  nn0opth2d  10985  facp1  10992  facdiv  11000  facndiv  11001  faclbnd  11003  faclbnd2  11004  faclbnd3  11005  bcval  11011  bccmpl  11016  bcm1k  11022  bcp1n  11023  bcp1nk  11024  bcval5  11025  bcp1m1  11027  bcpasc  11028  bcn2m1  11031  hashprg  11072  hashdifpr  11084  hashfzo  11086  hashfzp1  11088  hashfz0  11089  hashxp  11090  zfz1isolemsplit  11102  zfz1isolem1  11104  seq3coll  11106  lswwrd  11160  ccatfvalfi  11169  ccatass  11185  lswccatn0lsw  11188  wrdlenccats1lenm1g  11213  ccatw2s1leng  11215  ccatswrd  11251  ccatpfx  11282  swrdpfx  11288  pfxpfx  11289  ccats1pfxeq  11295  wrdeqs1cat  11301  wrdind  11303  wrd2ind  11304  pfxccatpfx2  11318  pfxccatin12d  11326  cats1catd  11349  cats2catd  11350  s2leng  11370  reval  11410  crre  11418  remim  11421  remul2  11434  immul2  11441  imval2  11455  cjdivap  11470  caucvgre  11542  cvg1nlemcau  11545  cvg1nlemres  11546  resqrexlemp1rp  11567  resqrexlemfp1  11570  resqrexlemover  11571  resqrexlemcalc1  11575  resqrexlemcalc3  11577  resqrexlemnm  11579  resqrexlemoverl  11582  resqrexlemglsq  11583  resqrexlemga  11584  resqrexlemsqa  11585  resqrexlemex  11586  resqrex  11587  sqrtdiv  11603  absvalsq  11614  absreimsq  11628  absdivap  11631  cau3lem  11675  maxabslemlub  11768  maxabslemval  11769  max0addsup  11780  minabs  11797  bdtrilem  11800  bdtri  11801  xrmaxaddlem  11821  xrmaxadd  11822  xrbdtri  11837  clim  11842  clim2  11844  climshftlemg  11863  climshft2  11867  climcn1  11869  climcn2  11870  subcn2  11872  reccn2ap  11874  climmulc2  11892  climsubc2  11894  clim2ser  11898  iser3shft  11907  climcau  11908  serf0  11913  fzosump1  11979  fsum1p  11980  fsump1  11982  sumsplitdc  11994  fsump1i  11995  mptfzshft  12004  fisum0diag2  12009  fsumconst  12016  fsumdifsnconst  12017  modfsummodlemstep  12019  modfsummod  12020  telfsumo  12028  fsumparts  12032  fsumrelem  12033  hash2iun1dif1  12042  binomlem  12045  binom  12046  binom1p  12047  binom1dif  12049  bcxmas  12051  isumsplit  12053  isum1p  12054  arisum  12060  arisum2  12061  trireciplem  12062  geoserap  12069  geolim  12073  geolim2  12074  georeclim  12075  geo2sum  12076  geoisum1  12081  cvgratnnlemseq  12088  cvgratnnlemsumlt  12090  cvgratnnlemfm  12091  cvgratz  12094  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  fprod1p  12161  fprodp1  12162  fprodcl2lem  12167  fprodfac  12177  fprodeq0  12179  fprodconst  12182  fprodrec  12191  fprodsplit1f  12196  fprodmodd  12203  efcllemp  12220  ef0lem  12222  efval  12223  esum  12224  ege2le3  12233  efaddlem  12236  efsep  12253  effsumlt  12254  eft0val  12255  efgt1p2  12257  efgt1p  12258  sinval  12264  cosval  12265  resinval  12277  recosval  12278  efi4p  12279  resin4p  12280  recos4p  12281  sinneg  12288  cosneg  12289  efival  12294  sinadd  12298  cosadd  12299  tanaddap  12301  sinmul  12306  cosmul  12307  cos2t  12312  cos2tsin  12313  ef01bndlem  12318  absefib  12333  demoivre  12335  demoivreALT  12336  eirraplem  12339  p1modz1  12356  dvdsmodexp  12357  moddvds  12361  mulmoddvds  12425  3dvds2dec  12428  zeo3  12430  odd2np1lem  12434  odd2np1  12435  oexpneg  12439  2tp1odd  12446  ltoddhalfle  12455  opoe  12457  opeo  12459  omeo  12460  m1expo  12462  m1exp1  12463  nn0o1gt2  12467  nn0o  12469  divalglemnn  12480  divalglemqt  12481  divalglemeunn  12483  divalglemex  12484  divalglemeuneg  12485  flodddiv4  12498  flodddiv4t2lthalf  12501  bitsp1o  12515  bitsmod  12518  bitsinv1lem  12523  gcdaddm  12556  bezoutlemnewy  12568  bezoutlema  12571  bezoutlemb  12572  bezoutlemex  12573  bezoutlemaz  12575  mulgcd  12588  gcddiv  12591  gcdmultiplez  12593  rpmulgcd  12598  rplpwr  12599  uzwodc  12609  lcmgcdlem  12650  lcmgcd  12651  divgcdcoprmex  12675  cncongr2  12677  prmexpb  12724  rpexp  12726  rpexp1i  12727  sqrt2irrlem  12734  oddpwdclemxy  12742  oddpwdclemndvds  12744  sqpweven  12748  2sqpwodd  12749  sqne2sq  12750  qmuldeneqnum  12768  nn0gcdsq  12773  zgcdsq  12774  numdensq  12775  dfphi2  12793  phiprmpw  12795  phiprm  12796  eulerthlema  12803  eulerthlemh  12804  eulerthlemth  12805  fermltl  12807  prmdiv  12808  prmdiveq  12809  prmdivdiv  12810  hashgcdlem  12811  odzval  12815  odzcllem  12816  odzdvds  12819  vfermltl  12825  powm2modprm  12826  reumodprminv  12827  modprm0  12828  nnnn0modprm0  12829  modprmn0modprm0  12830  coprimeprodsq  12831  coprimeprodsq2  12832  pythagtriplem1  12839  pythagtriplem3  12841  pythagtriplem4  12842  pythagtriplem6  12844  pythagtriplem7  12845  pythagtriplem12  12849  pythagtriplem14  12851  pythagtriplem15  12852  pythagtriplem16  12853  pythagtriplem17  12854  pythagtriplem18  12855  pceu  12869  pczpre  12871  pcdiv  12876  pcqdiv  12881  pcrec  12882  pczndvds  12890  pcneg  12899  pc2dvds  12904  pcprmpw2  12907  pcaddlem  12913  pcadd  12914  fldivp1  12922  pockthlem  12930  pockthi  12932  4sqlem5  12956  4sqlem9  12960  4sqlem10  12961  4sqlem2  12963  4sqlem3  12964  4sqlem4  12966  mul4sqlem  12967  4sqlem11  12975  4sqlem12  12976  4sqlem14  12978  4sqlem15  12979  4sqlem17  12981  4sqlem19  12983  ennnfonelemkh  13034  ennnfonelemhf1o  13035  setscomd  13124  ressressg  13159  qusex  13409  qusin  13410  grpinvalem  13469  grpinva  13470  grprida  13471  gsumsplit1r  13482  isnsgrp  13490  sgrpass  13492  sgrp1  13495  sgrppropd  13497  prdssgrpd  13499  mnd12g  13512  mndpropd  13524  prdsidlem  13531  prdsmndd  13532  imasmnd2  13536  mhmex  13546  mhmlin  13551  grprcan  13621  grpinvid1  13636  isgrpinv  13638  grplcan  13646  grpasscan1  13647  grplmulf1o  13658  grpinvadd  13662  grpinvsub  13666  grpsubsub4  13677  grppnpcan2  13678  grpnpncan  13679  dfgrp3mlem  13682  dfgrp3m  13683  grplactcnv  13686  prdsinvlem  13692  imasgrp2  13698  mhmlem  13702  mhmid  13703  mhmmnd  13704  mulgnnp1  13718  mulg2  13719  mulgnn0p1  13721  mulgsubcl  13724  mulgneg  13728  mulgaddcomlem  13733  mulgaddcom  13734  mulgz  13738  mulgnn0dir  13740  mulgdirlem  13741  mulgdir  13742  mulgneg2  13744  mulgnnass  13745  mulgnn0ass  13746  mulgass  13747  mulgassr  13748  mulgmodid  13749  mulgsubdir  13750  submmulg  13754  isnsg3  13795  nmzsubg  13798  ssnmz  13799  0nsg  13802  eqger  13812  eqgid  13814  eqgcpbl  13816  ghmlin  13836  ghmmulg  13844  ghmnsgima  13856  ghmnsgpreima  13857  conjghm  13864  conjnmz  13867  ablsub2inv  13899  abladdsub4  13902  abladdsub  13903  ablpncan2  13904  ablpnpcan  13908  ablnncan  13909  ablnnncan1  13912  gsumfzconst  13929  gsumfzsnfd  13933  gsumsplit0  13934  mgpress  13946  rngass  13954  rngdi  13955  rngdir  13956  rnglz  13960  rngmneg1  13962  rngsubdir  13967  rngpropd  13970  imasrng  13971  srgass  13986  srgmulgass  14004  srgpcomp  14005  srgpcompp  14006  srgpcomppsc  14007  ringpropd  14053  ringlz  14058  ring1eq0  14063  ringnegl  14066  ringmneg1  14068  ringsubdir  14072  mulgass2  14073  ring1  14074  imasring  14079  opprrng  14092  opprring  14094  unitgrp  14132  dvrcan1  14156  rdivmuldivd  14160  subrginv  14253  resrhm  14264  unitrrg  14283  islmod  14307  lmodlema  14308  islmodd  14309  lmod0vs  14337  lmodvs0  14338  lmodvsmmulgdi  14339  lmodvneg1  14346  lmodvsneg  14347  lmodsubvs  14359  lmodsubdi  14360  lmodsubdir  14361  lmodprop2d  14364  rmodislmodlem  14366  rmodislmod  14367  lsssetm  14372  islssmd  14375  lssclg  14380  lssvacl  14381  lss1d  14399  lsspropdg  14447  sraval  14453  rnglidlmcl  14496  gsumfzfsumlemm  14603  znunit  14675  mplsubgfilemcl  14715  resttop  14896  restco  14900  restin  14902  lmfval  14919  cnprcl2k  14932  txrest  15002  txdis1cn  15004  cnmpt2res  15023  psmettri2  15054  psmettri  15056  xmettri2  15087  xmettri  15098  mettri  15099  metrtri  15103  blvalps  15114  blval  15115  xblss2  15131  blhalf  15134  comet  15225  xmetxp  15233  txmetcnp  15244  cnmet  15256  ioo2bl  15277  ivthreinc  15371  limcmpted  15389  limcimolemlt  15390  cnplimclemr  15395  limccnp2cntop  15403  reldvg  15405  dvfvalap  15407  dvidlemap  15417  dvidrelem  15418  dvidsslem  15419  dvconst  15420  dvconstre  15422  dvconstss  15424  dvcnp2cntop  15425  dvaddxxbr  15427  dvmulxxbr  15428  dvcoapbr  15433  dvcjbr  15434  dvexp  15437  dvrecap  15439  dvmptcmulcn  15447  dveflem  15452  plyval  15458  elply2  15461  elplyr  15466  elplyd  15467  ply1termlem  15468  plyaddlem1  15473  plymullem1  15474  plycoeid3  15483  plycjlemc  15486  dvply1  15491  sin0pilem1  15507  sinperlem  15534  ptolemy  15550  tangtx  15564  abssinper  15572  reexplog  15597  relogexp  15598  cxprec  15636  rpdivcxp  15637  cxpmul  15638  rpabscxpbnd  15666  rplogbval  15671  rplogbreexp  15679  rprelogbmul  15681  logbrec  15686  logbgcd1irraplemap  15695  binom4  15705  wilthlem1  15706  mpodvdsmulf1o  15716  sgmppw  15718  0sgmppw  15719  1sgmprm  15720  1sgm2ppw  15721  perfectlem1  15725  perfectlem2  15726  perfect  15727  lgslem1  15731  lgslem4  15734  lgsval  15735  lgsfvalg  15736  lgsval2lem  15741  lgsval4lem  15742  lgsvalmod  15750  lgsneg  15755  lgsneg1  15756  lgsmod  15757  lgsdilem  15758  lgsdir2lem4  15762  lgsdir2  15764  lgsdirprm  15765  lgsdir  15766  lgsne0  15769  lgssq  15771  lgssq2  15772  lgsmulsqcoprm  15777  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem1a  15789  gausslemma2dlem4  15795  gausslemma2dlem5a  15796  gausslemma2dlem5  15797  gausslemma2dlem6  15798  gausslemma2dlem7  15799  gausslemma2d  15800  lgseisenlem1  15801  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgseisen  15805  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad2lem1  15812  lgsquad2lem2  15813  lgsquad3  15815  m1lgs  15816  2lgslem1a  15819  2lgslem1c  15821  2lgslem3a  15824  2lgslem3b  15825  2lgslem3c  15826  2lgslem3d  15827  2lgslem3a1  15828  2lgslem3b1  15829  2lgslem3c1  15830  2lgslem3d1  15831  2lgsoddprmlem1  15836  2lgsoddprmlem2  15837  2lgsoddprmlem3  15842  2sqlem1  15845  2sqlem2  15846  mul2sq  15847  2sqlem3  15848  2sqlem4  15849  2sqlem8  15854  2sqlem9  15855  2sqlem10  15856  vdegp1bid  16168  uspgr2wlkeqi  16220  isclwwlk  16247  clwwlkccatlem  16253  clwwlknonex2  16292  trilpolemeq1  16647  trilpolemlt1  16648  trirec0xor  16652  apdifflemf  16653  apdiff  16655  gsumgfsumlem  16686  gsumgfsum  16687