Theorem oveq1d 6022

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 6014	. 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 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  fvoveq1d  6029  csbov2g  6049  caovassg  6170  caovdig  6186  caovdirg  6189  caov12d  6193  caov31d  6194  caov411d  6197  caofinvl  6250  omsuc  6626  nnmsucr  6642  nnm1  6679  nnm2  6680  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  isacnm  7396  addasspig  7528  mulasspig  7530  mulpipq2  7569  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  archnqq  7615  prarloclemarch2  7617  enq0sym  7630  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  nqpnq0nq  7651  nq0m0r  7654  nq0a0  7655  nnanq0  7656  distrnq0  7657  addassnq0  7660  addpinq1  7662  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  prarloclemcalc  7700  addnqprllem  7725  addnqprulem  7726  appdivnq  7761  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  cauappcvgprlemladdru  7854  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemexb  7905  caucvgprprlem1  7907  addcmpblnr  7937  mulcmpblnrlemg  7938  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  ltsrprg  7945  1idsr  7966  pn0sr  7969  recexgt0sr  7971  mulgt0sr  7976  srpospr  7981  prsradd  7984  caucvgsrlemfv  7989  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffval  7994  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsrlembnd  7999  caucvgsr  8000  map2psrprg  8003  pitonnlem1p1  8044  pitonnlem2  8045  pitonn  8046  recidpirqlemcalc  8055  ax1rid  8075  axrnegex  8077  axcnre  8079  recriota  8088  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  mul12  8286  mul4  8289  muladd11  8290  readdcan  8297  muladd11r  8313  add12  8315  cnegex  8335  addcan  8337  negeu  8348  pncan2  8364  addsubass  8367  addsub  8368  2addsub  8371  addsubeq4  8372  subid  8376  subid1  8377  npncan  8378  nppcan  8379  nnpcan  8380  nnncan1  8393  npncan3  8395  pnpcan  8396  pnncan  8398  ppncan  8399  addsub4  8400  negsub  8405  subneg  8406  subeqxfrd  8520  mvlraddd  8521  mvlladdd  8522  mvrraddd  8523  subaddeqd  8526  ine0  8551  mulneg1  8552  ltadd2  8577  apreap  8745  cru  8760  recexap  8811  mulcanapd  8819  div23ap  8849  div13ap  8851  divmulassap  8853  divmulasscomap  8854  divcanap4  8857  muldivdirap  8865  divsubdirap  8866  divmuldivap  8870  divdivdivap  8871  divcanap5  8872  divmul13ap  8873  divmuleqap  8875  divdiv32ap  8878  divcanap7  8879  dmdcanap  8880  divdivap1  8881  divdivap2  8882  divadddivap  8885  divsubdivap  8886  conjmulap  8887  divneg2ap  8894  subrecap  8997  mvllmulapd  9000  lt2mul2div  9037  nndivtr  9163  2halves  9351  halfaddsub  9356  subhalfhalf  9357  avgle1  9363  avgle2  9364  div4p1lem1div2  9376  un0addcl  9413  un0mulcl  9414  peano2z  9493  zneo  9559  nneoor  9560  nneo  9561  zeo  9563  zeo2  9564  deceq1  9593  qreccl  9849  xaddcom  10069  xnegdi  10076  xaddass  10077  xaddass2  10078  xpncan  10079  xleadd1a  10081  xltadd1  10084  xposdif  10090  xadd4d  10093  lincmb01cmp  10211  iccf1o  10212  fz0to4untppr  10332  fzo0addel  10406  fzosubel3  10414  qavgle  10490  2tnp1ge0ge0  10533  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  ceilqm1lt  10546  flqdiv  10555  modqlt  10567  modqdiffl  10569  modqcyc2  10594  modqaddabs  10596  mulqaddmodid  10598  mulp1mod1  10599  modqmuladd  10600  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  addmodidr  10607  modqadd2mod  10608  modqm1p1mod0  10609  modqmul12d  10612  modqnegd  10613  modqadd12d  10614  modqsub12d  10615  q2submod  10619  modqmulmodr  10624  modqaddmulmod  10625  modqsubdir  10627  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecuzrdgsuc  10648  frecfzennn  10660  iseqovex  10692  seq3-1p  10724  seq3caopr2  10727  seqcaopr2g  10728  seq3caopr  10729  seqcaoprg  10730  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3id  10759  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  expp1  10780  exprecap  10814  expaddzaplem  10816  expmulzap  10819  expdivap  10824  sqval  10831  sqsubswap  10833  sqdividap  10838  subsq  10880  subsq2  10881  binom2  10885  binom2sub  10887  mulbinom2  10890  binom3  10891  zesq  10892  bernneq2  10895  modqexp  10900  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  nn0opthd  10956  nn0opth2d  10957  facp1  10964  facdiv  10972  facndiv  10973  faclbnd  10975  faclbnd2  10976  faclbnd3  10977  bcval  10983  bccmpl  10988  bcm1k  10994  bcp1n  10995  bcp1nk  10996  bcval5  10997  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  hashprg  11043  hashdifpr  11055  hashfzo  11057  hashfzp1  11059  hashfz0  11060  hashxp  11061  zfz1isolemsplit  11073  zfz1isolem1  11075  seq3coll  11077  lswwrd  11131  ccatfvalfi  11140  ccatass  11156  lswccatn0lsw  11159  wrdlenccats1lenm1g  11184  ccatswrd  11218  ccatpfx  11249  swrdpfx  11255  pfxpfx  11256  ccats1pfxeq  11262  wrdeqs1cat  11268  wrdind  11270  wrd2ind  11271  pfxccatpfx2  11285  pfxccatin12d  11293  cats1catd  11316  cats2catd  11317  s2leng  11337  reval  11376  crre  11384  remim  11387  remul2  11400  immul2  11407  imval2  11421  cjdivap  11436  caucvgre  11508  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemp1rp  11533  resqrexlemfp1  11536  resqrexlemover  11537  resqrexlemcalc1  11541  resqrexlemcalc3  11543  resqrexlemnm  11545  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemga  11550  resqrexlemsqa  11551  resqrexlemex  11552  resqrex  11553  sqrtdiv  11569  absvalsq  11580  absreimsq  11594  absdivap  11597  cau3lem  11641  maxabslemlub  11734  maxabslemval  11735  max0addsup  11746  minabs  11763  bdtrilem  11766  bdtri  11767  xrmaxaddlem  11787  xrmaxadd  11788  xrbdtri  11803  clim  11808  clim2  11810  climshftlemg  11829  climshft2  11833  climcn1  11835  climcn2  11836  subcn2  11838  reccn2ap  11840  climmulc2  11858  climsubc2  11860  clim2ser  11864  iser3shft  11873  climcau  11874  serf0  11879  fzosump1  11944  fsum1p  11945  fsump1  11947  sumsplitdc  11959  fsump1i  11960  mptfzshft  11969  fisum0diag2  11974  fsumconst  11981  fsumdifsnconst  11982  modfsummodlemstep  11984  modfsummod  11985  telfsumo  11993  fsumparts  11997  fsumrelem  11998  hash2iun1dif1  12007  binomlem  12010  binom  12011  binom1p  12012  binom1dif  12014  bcxmas  12016  isumsplit  12018  isum1p  12019  arisum  12025  arisum2  12026  trireciplem  12027  geoserap  12034  geolim  12038  geolim2  12039  georeclim  12040  geo2sum  12041  geoisum1  12046  cvgratnnlemseq  12053  cvgratnnlemsumlt  12055  cvgratnnlemfm  12056  cvgratz  12059  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  fprod1p  12126  fprodp1  12127  fprodcl2lem  12132  fprodfac  12142  fprodeq0  12144  fprodconst  12147  fprodrec  12156  fprodsplit1f  12161  fprodmodd  12168  efcllemp  12185  ef0lem  12187  efval  12188  esum  12189  ege2le3  12198  efaddlem  12201  efsep  12218  effsumlt  12219  eft0val  12220  efgt1p2  12222  efgt1p  12223  sinval  12229  cosval  12230  resinval  12242  recosval  12243  efi4p  12244  resin4p  12245  recos4p  12246  sinneg  12253  cosneg  12254  efival  12259  sinadd  12263  cosadd  12264  tanaddap  12266  sinmul  12271  cosmul  12272  cos2t  12277  cos2tsin  12278  ef01bndlem  12283  absefib  12298  demoivre  12300  demoivreALT  12301  eirraplem  12304  p1modz1  12321  dvdsmodexp  12322  moddvds  12326  mulmoddvds  12390  3dvds2dec  12393  zeo3  12395  odd2np1lem  12399  odd2np1  12400  oexpneg  12404  2tp1odd  12411  ltoddhalfle  12420  opoe  12422  opeo  12424  omeo  12425  m1expo  12427  m1exp1  12428  nn0o1gt2  12432  nn0o  12434  divalglemnn  12445  divalglemqt  12446  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  flodddiv4  12463  flodddiv4t2lthalf  12466  bitsp1o  12480  bitsmod  12483  bitsinv1lem  12488  gcdaddm  12521  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  bezoutlemex  12538  bezoutlemaz  12540  mulgcd  12553  gcddiv  12556  gcdmultiplez  12558  rpmulgcd  12563  rplpwr  12564  uzwodc  12574  lcmgcdlem  12615  lcmgcd  12616  divgcdcoprmex  12640  cncongr2  12642  prmexpb  12689  rpexp  12691  rpexp1i  12692  sqrt2irrlem  12699  oddpwdclemxy  12707  oddpwdclemndvds  12709  sqpweven  12713  2sqpwodd  12714  sqne2sq  12715  qmuldeneqnum  12733  nn0gcdsq  12738  zgcdsq  12739  numdensq  12740  dfphi2  12758  phiprmpw  12760  phiprm  12761  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  fermltl  12772  prmdiv  12773  prmdiveq  12774  prmdivdiv  12775  hashgcdlem  12776  odzval  12780  odzcllem  12781  odzdvds  12784  vfermltl  12790  powm2modprm  12791  reumodprminv  12792  modprm0  12793  nnnn0modprm0  12794  modprmn0modprm0  12795  coprimeprodsq  12796  coprimeprodsq2  12797  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem4  12807  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem15  12817  pythagtriplem16  12818  pythagtriplem17  12819  pythagtriplem18  12820  pceu  12834  pczpre  12836  pcdiv  12841  pcqdiv  12846  pcrec  12847  pczndvds  12855  pcneg  12864  pc2dvds  12869  pcprmpw2  12872  pcaddlem  12878  pcadd  12879  fldivp1  12887  pockthlem  12895  pockthi  12897  4sqlem5  12921  4sqlem9  12925  4sqlem10  12926  4sqlem2  12928  4sqlem3  12929  4sqlem4  12931  mul4sqlem  12932  4sqlem11  12940  4sqlem12  12941  4sqlem14  12943  4sqlem15  12944  4sqlem17  12946  4sqlem19  12948  ennnfonelemkh  12999  ennnfonelemhf1o  13000  setscomd  13089  ressressg  13124  qusex  13374  qusin  13375  grpinvalem  13434  grpinva  13435  grprida  13436  gsumsplit1r  13447  isnsgrp  13455  sgrpass  13457  sgrp1  13460  sgrppropd  13462  prdssgrpd  13464  mnd12g  13477  mndpropd  13489  prdsidlem  13496  prdsmndd  13497  imasmnd2  13501  mhmex  13511  mhmlin  13516  grprcan  13586  grpinvid1  13601  isgrpinv  13603  grplcan  13611  grpasscan1  13612  grplmulf1o  13623  grpinvadd  13627  grpinvsub  13631  grpsubsub4  13642  grppnpcan2  13643  grpnpncan  13644  dfgrp3mlem  13647  dfgrp3m  13648  grplactcnv  13651  prdsinvlem  13657  imasgrp2  13663  mhmlem  13667  mhmid  13668  mhmmnd  13669  mulgnnp1  13683  mulg2  13684  mulgnn0p1  13686  mulgsubcl  13689  mulgneg  13693  mulgaddcomlem  13698  mulgaddcom  13699  mulgz  13703  mulgnn0dir  13705  mulgdirlem  13706  mulgdir  13707  mulgneg2  13709  mulgnnass  13710  mulgnn0ass  13711  mulgass  13712  mulgassr  13713  mulgmodid  13714  mulgsubdir  13715  submmulg  13719  isnsg3  13760  nmzsubg  13763  ssnmz  13764  0nsg  13767  eqger  13777  eqgid  13779  eqgcpbl  13781  ghmlin  13801  ghmmulg  13809  ghmnsgima  13821  ghmnsgpreima  13822  conjghm  13829  conjnmz  13832  ablsub2inv  13864  abladdsub4  13867  abladdsub  13868  ablpncan2  13869  ablpnpcan  13873  ablnncan  13874  ablnnncan1  13877  gsumfzconst  13894  gsumfzsnfd  13898  mgpress  13910  rngass  13918  rngdi  13919  rngdir  13920  rnglz  13924  rngmneg1  13926  rngsubdir  13931  rngpropd  13934  imasrng  13935  srgass  13950  srgmulgass  13968  srgpcomp  13969  srgpcompp  13970  srgpcomppsc  13971  ringpropd  14017  ringlz  14022  ring1eq0  14027  ringnegl  14030  ringmneg1  14032  ringsubdir  14036  mulgass2  14037  ring1  14038  imasring  14043  opprrng  14056  opprring  14058  unitgrp  14096  dvrcan1  14120  rdivmuldivd  14124  subrginv  14217  resrhm  14228  unitrrg  14247  islmod  14271  lmodlema  14272  islmodd  14273  lmod0vs  14301  lmodvs0  14302  lmodvsmmulgdi  14303  lmodvneg1  14310  lmodvsneg  14311  lmodsubvs  14323  lmodsubdi  14324  lmodsubdir  14325  lmodprop2d  14328  rmodislmodlem  14330  rmodislmod  14331  lsssetm  14336  islssmd  14339  lssclg  14344  lssvacl  14345  lss1d  14363  lsspropdg  14411  sraval  14417  rnglidlmcl  14460  gsumfzfsumlemm  14567  znunit  14639  mplsubgfilemcl  14679  resttop  14860  restco  14864  restin  14866  lmfval  14883  cnprcl2k  14896  txrest  14966  txdis1cn  14968  cnmpt2res  14987  psmettri2  15018  psmettri  15020  xmettri2  15051  xmettri  15062  mettri  15063  metrtri  15067  blvalps  15078  blval  15079  xblss2  15095  blhalf  15098  comet  15189  xmetxp  15197  txmetcnp  15208  cnmet  15220  ioo2bl  15241  ivthreinc  15335  limcmpted  15353  limcimolemlt  15354  cnplimclemr  15359  limccnp2cntop  15367  reldvg  15369  dvfvalap  15371  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvconst  15384  dvconstre  15386  dvconstss  15388  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvexp  15401  dvrecap  15403  dvmptcmulcn  15411  dveflem  15416  plyval  15422  elply2  15425  elplyr  15430  elplyd  15431  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycjlemc  15450  dvply1  15455  sin0pilem1  15471  sinperlem  15498  ptolemy  15514  tangtx  15528  abssinper  15536  reexplog  15561  relogexp  15562  cxprec  15600  rpdivcxp  15601  cxpmul  15602  rpabscxpbnd  15630  rplogbval  15635  rplogbreexp  15643  rprelogbmul  15645  logbrec  15650  logbgcd1irraplemap  15659  binom4  15669  wilthlem1  15670  mpodvdsmulf1o  15680  sgmppw  15682  0sgmppw  15683  1sgmprm  15684  1sgm2ppw  15685  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgslem1  15695  lgslem4  15698  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsval4lem  15706  lgsvalmod  15714  lgsneg  15719  lgsneg1  15720  lgsmod  15721  lgsdilem  15722  lgsdir2lem4  15726  lgsdir2  15728  lgsdirprm  15729  lgsdir  15730  lgsne0  15733  lgssq  15735  lgssq2  15736  lgsmulsqcoprm  15741  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem1a  15753  gausslemma2dlem4  15759  gausslemma2dlem5a  15760  gausslemma2dlem5  15761  gausslemma2dlem6  15762  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  lgsquad2lem2  15777  lgsquad3  15779  m1lgs  15780  2lgslem1a  15783  2lgslem1c  15785  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2lgsoddprmlem1  15800  2lgsoddprmlem2  15801  2lgsoddprmlem3  15806  2sqlem1  15809  2sqlem2  15810  mul2sq  15811  2sqlem3  15812  2sqlem4  15813  2sqlem8  15818  2sqlem9  15819  2sqlem10  15820  uspgr2wlkeqi  16113  isclwwlk  16137  clwwlkccatlem  16143  trilpolemeq1  16496  trilpolemlt1  16497  trirec0xor  16501  apdifflemf  16502  apdiff  16504