Theorem oveq1d 5961

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 5953	. 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 1373  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  fvoveq1d  5968  csbov2g  5988  caovassg  6107  caovdig  6123  caovdirg  6126  caov12d  6130  caov31d  6131  caov411d  6134  caofinvl  6186  omsuc  6560  nnmsucr  6576  nnm1  6613  nnm2  6614  ecovass  6733  ecoviass  6734  ecovdi  6735  ecovidi  6736  isacnm  7317  addasspig  7445  mulasspig  7447  mulpipq2  7486  distrnqg  7502  ltsonq  7513  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  archnqq  7532  prarloclemarch2  7534  enq0sym  7547  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  nqpnq0nq  7568  nq0m0r  7571  nq0a0  7572  nnanq0  7573  distrnq0  7574  addassnq0  7577  addpinq1  7579  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  prarloclemcalc  7617  addnqprllem  7642  addnqprulem  7643  appdivnq  7678  recexprlem1ssl  7748  recexprlem1ssu  7749  ltmprr  7757  cauappcvgprlemladdru  7771  cauappcvgprlem1  7774  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemexb  7822  caucvgprprlem1  7824  addcmpblnr  7854  mulcmpblnrlemg  7855  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  ltsrprg  7862  1idsr  7883  pn0sr  7886  recexgt0sr  7888  mulgt0sr  7893  srpospr  7898  prsradd  7901  caucvgsrlemfv  7906  caucvgsrlemcau  7908  caucvgsrlemgt1  7910  caucvgsrlemoffval  7911  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  caucvgsrlembnd  7916  caucvgsr  7917  map2psrprg  7920  pitonnlem1p1  7961  pitonnlem2  7962  pitonn  7963  recidpirqlemcalc  7972  ax1rid  7992  axrnegex  7994  axcnre  7996  recriota  8005  nntopi  8009  axcaucvglemval  8012  axcaucvglemcau  8013  axcaucvglemres  8014  mul12  8203  mul4  8206  muladd11  8207  readdcan  8214  muladd11r  8230  add12  8232  cnegex  8252  addcan  8254  negeu  8265  pncan2  8281  addsubass  8284  addsub  8285  2addsub  8288  addsubeq4  8289  subid  8293  subid1  8294  npncan  8295  nppcan  8296  nnpcan  8297  nnncan1  8310  npncan3  8312  pnpcan  8313  pnncan  8315  ppncan  8316  addsub4  8317  negsub  8322  subneg  8323  subeqxfrd  8437  mvlraddd  8438  mvlladdd  8439  mvrraddd  8440  subaddeqd  8443  ine0  8468  mulneg1  8469  ltadd2  8494  apreap  8662  cru  8677  recexap  8728  mulcanapd  8736  div23ap  8766  div13ap  8768  divmulassap  8770  divmulasscomap  8771  divcanap4  8774  muldivdirap  8782  divsubdirap  8783  divmuldivap  8787  divdivdivap  8788  divcanap5  8789  divmul13ap  8790  divmuleqap  8792  divdiv32ap  8795  divcanap7  8796  dmdcanap  8797  divdivap1  8798  divdivap2  8799  divadddivap  8802  divsubdivap  8803  conjmulap  8804  divneg2ap  8811  subrecap  8914  mvllmulapd  8917  lt2mul2div  8954  nndivtr  9080  2halves  9268  halfaddsub  9273  subhalfhalf  9274  avgle1  9280  avgle2  9281  div4p1lem1div2  9293  un0addcl  9330  un0mulcl  9331  peano2z  9410  zneo  9476  nneoor  9477  nneo  9478  zeo  9480  zeo2  9481  deceq1  9510  qreccl  9765  xaddcom  9985  xnegdi  9992  xaddass  9993  xaddass2  9994  xpncan  9995  xleadd1a  9997  xltadd1  10000  xposdif  10006  xadd4d  10009  lincmb01cmp  10127  iccf1o  10128  fz0to4untppr  10248  fzo0addel  10319  fzosubel3  10327  qavgle  10403  2tnp1ge0ge0  10446  fldiv4p1lem1div2  10450  fldiv4lem1div2  10452  ceilqm1lt  10459  flqdiv  10468  modqlt  10480  modqdiffl  10482  modqcyc2  10507  modqaddabs  10509  mulqaddmodid  10511  mulp1mod1  10512  modqmuladd  10513  modqmuladdnn0  10515  qnegmod  10516  addmodid  10519  addmodidr  10520  modqadd2mod  10521  modqm1p1mod0  10522  modqmul12d  10525  modqnegd  10526  modqadd12d  10527  modqsub12d  10528  q2submod  10532  modqmulmodr  10537  modqaddmulmod  10538  modqsubdir  10540  modfzo0difsn  10542  modsumfzodifsn  10543  addmodlteq  10545  frecuzrdgsuc  10561  frecfzennn  10573  iseqovex  10605  seq3-1p  10637  seq3caopr2  10640  seqcaopr2g  10641  seq3caopr  10642  seqcaoprg  10643  seqf1oglem2a  10665  seqf1oglem1  10666  seqf1oglem2  10667  seq3id  10672  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  expp1  10693  exprecap  10727  expaddzaplem  10729  expmulzap  10732  expdivap  10737  sqval  10744  sqsubswap  10746  sqdividap  10751  subsq  10793  subsq2  10794  binom2  10798  binom2sub  10800  mulbinom2  10803  binom3  10804  zesq  10805  bernneq2  10808  modqexp  10813  sqoddm1div8  10840  mulsubdivbinom2ap  10858  nn0opthlem1d  10867  nn0opthd  10869  nn0opth2d  10870  facp1  10877  facdiv  10885  facndiv  10886  faclbnd  10888  faclbnd2  10889  faclbnd3  10890  bcval  10896  bccmpl  10901  bcm1k  10907  bcp1n  10908  bcp1nk  10909  bcval5  10910  bcp1m1  10912  bcpasc  10913  bcn2m1  10916  hashprg  10955  hashdifpr  10967  hashfzo  10969  hashfzp1  10971  hashfz0  10972  hashxp  10973  zfz1isolemsplit  10985  zfz1isolem1  10987  seq3coll  10989  lswwrd  11042  ccatfvalfi  11051  ccatass  11067  lswccatn0lsw  11070  ccatswrd  11126  ccatpfx  11155  reval  11193  crre  11201  remim  11204  remul2  11217  immul2  11224  imval2  11238  cjdivap  11253  caucvgre  11325  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemp1rp  11350  resqrexlemfp1  11353  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemcalc3  11360  resqrexlemnm  11362  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemga  11367  resqrexlemsqa  11368  resqrexlemex  11369  resqrex  11370  sqrtdiv  11386  absvalsq  11397  absreimsq  11411  absdivap  11414  cau3lem  11458  maxabslemlub  11551  maxabslemval  11552  max0addsup  11563  minabs  11580  bdtrilem  11583  bdtri  11584  xrmaxaddlem  11604  xrmaxadd  11605  xrbdtri  11620  clim  11625  clim2  11627  climshftlemg  11646  climshft2  11650  climcn1  11652  climcn2  11653  subcn2  11655  reccn2ap  11657  climmulc2  11675  climsubc2  11677  clim2ser  11681  iser3shft  11690  climcau  11691  serf0  11696  fzosump1  11761  fsum1p  11762  fsump1  11764  sumsplitdc  11776  fsump1i  11777  mptfzshft  11786  fisum0diag2  11791  fsumconst  11798  fsumdifsnconst  11799  modfsummodlemstep  11801  modfsummod  11802  telfsumo  11810  fsumparts  11814  fsumrelem  11815  hash2iun1dif1  11824  binomlem  11827  binom  11828  binom1p  11829  binom1dif  11831  bcxmas  11833  isumsplit  11835  isum1p  11836  arisum  11842  arisum2  11843  trireciplem  11844  geoserap  11851  geolim  11855  geolim2  11856  georeclim  11857  geo2sum  11858  geoisum1  11863  cvgratnnlemseq  11870  cvgratnnlemsumlt  11872  cvgratnnlemfm  11873  cvgratz  11876  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  fprod1p  11943  fprodp1  11944  fprodcl2lem  11949  fprodfac  11959  fprodeq0  11961  fprodconst  11964  fprodrec  11973  fprodsplit1f  11978  fprodmodd  11985  efcllemp  12002  ef0lem  12004  efval  12005  esum  12006  ege2le3  12015  efaddlem  12018  efsep  12035  effsumlt  12036  eft0val  12037  efgt1p2  12039  efgt1p  12040  sinval  12046  cosval  12047  resinval  12059  recosval  12060  efi4p  12061  resin4p  12062  recos4p  12063  sinneg  12070  cosneg  12071  efival  12076  sinadd  12080  cosadd  12081  tanaddap  12083  sinmul  12088  cosmul  12089  cos2t  12094  cos2tsin  12095  ef01bndlem  12100  absefib  12115  demoivre  12117  demoivreALT  12118  eirraplem  12121  p1modz1  12138  dvdsmodexp  12139  moddvds  12143  mulmoddvds  12207  3dvds2dec  12210  zeo3  12212  odd2np1lem  12216  odd2np1  12217  oexpneg  12221  2tp1odd  12228  ltoddhalfle  12237  opoe  12239  opeo  12241  omeo  12242  m1expo  12244  m1exp1  12245  nn0o1gt2  12249  nn0o  12251  divalglemnn  12262  divalglemqt  12263  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  flodddiv4  12280  flodddiv4t2lthalf  12283  bitsp1o  12297  bitsmod  12300  bitsinv1lem  12305  gcdaddm  12338  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  bezoutlemex  12355  bezoutlemaz  12357  mulgcd  12370  gcddiv  12373  gcdmultiplez  12375  rpmulgcd  12380  rplpwr  12381  uzwodc  12391  lcmgcdlem  12432  lcmgcd  12433  divgcdcoprmex  12457  cncongr2  12459  prmexpb  12506  rpexp  12508  rpexp1i  12509  sqrt2irrlem  12516  oddpwdclemxy  12524  oddpwdclemndvds  12526  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  qmuldeneqnum  12550  nn0gcdsq  12555  zgcdsq  12556  numdensq  12557  dfphi2  12575  phiprmpw  12577  phiprm  12578  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  fermltl  12589  prmdiv  12590  prmdiveq  12591  prmdivdiv  12592  hashgcdlem  12593  odzval  12597  odzcllem  12598  odzdvds  12601  vfermltl  12607  powm2modprm  12608  reumodprminv  12609  modprm0  12610  nnnn0modprm0  12611  modprmn0modprm0  12612  coprimeprodsq  12613  coprimeprodsq2  12614  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem4  12624  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem15  12634  pythagtriplem16  12635  pythagtriplem17  12636  pythagtriplem18  12637  pceu  12651  pczpre  12653  pcdiv  12658  pcqdiv  12663  pcrec  12664  pczndvds  12672  pcneg  12681  pc2dvds  12686  pcprmpw2  12689  pcaddlem  12695  pcadd  12696  fldivp1  12704  pockthlem  12712  pockthi  12714  4sqlem5  12738  4sqlem9  12742  4sqlem10  12743  4sqlem2  12745  4sqlem3  12746  4sqlem4  12748  mul4sqlem  12749  4sqlem11  12757  4sqlem12  12758  4sqlem14  12760  4sqlem15  12761  4sqlem17  12763  4sqlem19  12765  ennnfonelemkh  12816  ennnfonelemhf1o  12817  setscomd  12906  ressressg  12940  qusex  13190  qusin  13191  grpinvalem  13250  grpinva  13251  grprida  13252  gsumsplit1r  13263  isnsgrp  13271  sgrpass  13273  sgrp1  13276  sgrppropd  13278  prdssgrpd  13280  mnd12g  13293  mndpropd  13305  prdsidlem  13312  prdsmndd  13313  imasmnd2  13317  mhmex  13327  mhmlin  13332  grprcan  13402  grpinvid1  13417  isgrpinv  13419  grplcan  13427  grpasscan1  13428  grplmulf1o  13439  grpinvadd  13443  grpinvsub  13447  grpsubsub4  13458  grppnpcan2  13459  grpnpncan  13460  dfgrp3mlem  13463  dfgrp3m  13464  grplactcnv  13467  prdsinvlem  13473  imasgrp2  13479  mhmlem  13483  mhmid  13484  mhmmnd  13485  mulgnnp1  13499  mulg2  13500  mulgnn0p1  13502  mulgsubcl  13505  mulgneg  13509  mulgaddcomlem  13514  mulgaddcom  13515  mulgz  13519  mulgnn0dir  13521  mulgdirlem  13522  mulgdir  13523  mulgneg2  13525  mulgnnass  13526  mulgnn0ass  13527  mulgass  13528  mulgassr  13529  mulgmodid  13530  mulgsubdir  13531  submmulg  13535  isnsg3  13576  nmzsubg  13579  ssnmz  13580  0nsg  13583  eqger  13593  eqgid  13595  eqgcpbl  13597  ghmlin  13617  ghmmulg  13625  ghmnsgima  13637  ghmnsgpreima  13638  conjghm  13645  conjnmz  13648  ablsub2inv  13680  abladdsub4  13683  abladdsub  13684  ablpncan2  13685  ablpnpcan  13689  ablnncan  13690  ablnnncan1  13693  gsumfzconst  13710  gsumfzsnfd  13714  mgpress  13726  rngass  13734  rngdi  13735  rngdir  13736  rnglz  13740  rngmneg1  13742  rngsubdir  13747  rngpropd  13750  imasrng  13751  srgass  13766  srgmulgass  13784  srgpcomp  13785  srgpcompp  13786  srgpcomppsc  13787  ringpropd  13833  ringlz  13838  ring1eq0  13843  ringnegl  13846  ringmneg1  13848  ringsubdir  13852  mulgass2  13853  ring1  13854  imasring  13859  opprrng  13872  opprring  13874  unitgrp  13911  dvrcan1  13935  rdivmuldivd  13939  subrginv  14032  resrhm  14043  unitrrg  14062  islmod  14086  lmodlema  14087  islmodd  14088  lmod0vs  14116  lmodvs0  14117  lmodvsmmulgdi  14118  lmodvneg1  14125  lmodvsneg  14126  lmodsubvs  14138  lmodsubdi  14139  lmodsubdir  14140  lmodprop2d  14143  rmodislmodlem  14145  rmodislmod  14146  lsssetm  14151  islssmd  14154  lssclg  14159  lssvacl  14160  lss1d  14178  lsspropdg  14226  sraval  14232  rnglidlmcl  14275  gsumfzfsumlemm  14382  znunit  14454  mplsubgfilemcl  14494  resttop  14675  restco  14679  restin  14681  lmfval  14697  cnprcl2k  14711  txrest  14781  txdis1cn  14783  cnmpt2res  14802  psmettri2  14833  psmettri  14835  xmettri2  14866  xmettri  14877  mettri  14878  metrtri  14882  blvalps  14893  blval  14894  xblss2  14910  blhalf  14913  comet  15004  xmetxp  15012  txmetcnp  15023  cnmet  15035  ioo2bl  15056  ivthreinc  15150  limcmpted  15168  limcimolemlt  15169  cnplimclemr  15174  limccnp2cntop  15182  reldvg  15184  dvfvalap  15186  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvconst  15199  dvconstre  15201  dvconstss  15203  dvcnp2cntop  15204  dvaddxxbr  15206  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvexp  15216  dvrecap  15218  dvmptcmulcn  15226  dveflem  15231  plyval  15237  elply2  15240  elplyr  15245  elplyd  15246  ply1termlem  15247  plyaddlem1  15252  plymullem1  15253  plycoeid3  15262  plycjlemc  15265  dvply1  15270  sin0pilem1  15286  sinperlem  15313  ptolemy  15329  tangtx  15343  abssinper  15351  reexplog  15376  relogexp  15377  cxprec  15415  rpdivcxp  15416  cxpmul  15417  rpabscxpbnd  15445  rplogbval  15450  rplogbreexp  15458  rprelogbmul  15460  logbrec  15465  logbgcd1irraplemap  15474  binom4  15484  wilthlem1  15485  mpodvdsmulf1o  15495  sgmppw  15497  0sgmppw  15498  1sgmprm  15499  1sgm2ppw  15500  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgslem1  15510  lgslem4  15513  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsval4lem  15521  lgsvalmod  15529  lgsneg  15534  lgsneg1  15535  lgsmod  15536  lgsdilem  15537  lgsdir2lem4  15541  lgsdir2  15543  lgsdirprm  15544  lgsdir  15545  lgsne0  15548  lgssq  15550  lgssq2  15551  lgsmulsqcoprm  15556  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1a  15568  gausslemma2dlem4  15574  gausslemma2dlem5a  15575  gausslemma2dlem5  15576  gausslemma2dlem6  15577  gausslemma2dlem7  15578  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  lgsquad2lem2  15592  lgsquad3  15594  m1lgs  15595  2lgslem1a  15598  2lgslem1c  15600  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  2lgsoddprmlem1  15615  2lgsoddprmlem2  15616  2lgsoddprmlem3  15621  2sqlem1  15624  2sqlem2  15625  mul2sq  15626  2sqlem3  15627  2sqlem4  15628  2sqlem8  15633  2sqlem9  15634  2sqlem10  15635  trilpolemeq1  16016  trilpolemlt1  16017  trirec0xor  16021  apdifflemf  16022  apdiff  16024