Theorem oveq1d 5940

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 5932	. 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 1364  (class class class)co 5925

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  fvoveq1d  5947  csbov2g  5967  caovassg  6086  caovdig  6102  caovdirg  6105  caov12d  6109  caov31d  6110  caov411d  6113  caofinvl  6165  omsuc  6539  nnmsucr  6555  nnm1  6592  nnm2  6593  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  isacnm  7286  addasspig  7414  mulasspig  7416  mulpipq2  7455  distrnqg  7471  ltsonq  7482  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  archnqq  7501  prarloclemarch2  7503  enq0sym  7516  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  nqpnq0nq  7537  nq0m0r  7540  nq0a0  7541  nnanq0  7542  distrnq0  7543  addassnq0  7546  addpinq1  7548  prarloclemlo  7578  prarloclem3  7581  prarloclem5  7584  prarloclemcalc  7586  addnqprllem  7611  addnqprulem  7612  appdivnq  7647  recexprlem1ssl  7717  recexprlem1ssu  7718  ltmprr  7726  cauappcvgprlemladdru  7740  cauappcvgprlem1  7743  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemexb  7791  caucvgprprlem1  7793  addcmpblnr  7823  mulcmpblnrlemg  7824  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  ltsrprg  7831  1idsr  7852  pn0sr  7855  recexgt0sr  7857  mulgt0sr  7862  srpospr  7867  prsradd  7870  caucvgsrlemfv  7875  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffval  7880  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  caucvgsrlembnd  7885  caucvgsr  7886  map2psrprg  7889  pitonnlem1p1  7930  pitonnlem2  7931  pitonn  7932  recidpirqlemcalc  7941  ax1rid  7961  axrnegex  7963  axcnre  7965  recriota  7974  nntopi  7978  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  mul12  8172  mul4  8175  muladd11  8176  readdcan  8183  muladd11r  8199  add12  8201  cnegex  8221  addcan  8223  negeu  8234  pncan2  8250  addsubass  8253  addsub  8254  2addsub  8257  addsubeq4  8258  subid  8262  subid1  8263  npncan  8264  nppcan  8265  nnpcan  8266  nnncan1  8279  npncan3  8281  pnpcan  8282  pnncan  8284  ppncan  8285  addsub4  8286  negsub  8291  subneg  8292  subeqxfrd  8406  mvlraddd  8407  mvlladdd  8408  mvrraddd  8409  subaddeqd  8412  ine0  8437  mulneg1  8438  ltadd2  8463  apreap  8631  cru  8646  recexap  8697  mulcanapd  8705  div23ap  8735  div13ap  8737  divmulassap  8739  divmulasscomap  8740  divcanap4  8743  muldivdirap  8751  divsubdirap  8752  divmuldivap  8756  divdivdivap  8757  divcanap5  8758  divmul13ap  8759  divmuleqap  8761  divdiv32ap  8764  divcanap7  8765  dmdcanap  8766  divdivap1  8767  divdivap2  8768  divadddivap  8771  divsubdivap  8772  conjmulap  8773  divneg2ap  8780  subrecap  8883  mvllmulapd  8886  lt2mul2div  8923  nndivtr  9049  2halves  9237  halfaddsub  9242  subhalfhalf  9243  avgle1  9249  avgle2  9250  div4p1lem1div2  9262  un0addcl  9299  un0mulcl  9300  peano2z  9379  zneo  9444  nneoor  9445  nneo  9446  zeo  9448  zeo2  9449  deceq1  9478  qreccl  9733  xaddcom  9953  xnegdi  9960  xaddass  9961  xaddass2  9962  xpncan  9963  xleadd1a  9965  xltadd1  9968  xposdif  9974  xadd4d  9977  lincmb01cmp  10095  iccf1o  10096  fz0to4untppr  10216  fzosubel3  10289  qavgle  10365  2tnp1ge0ge0  10408  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  ceilqm1lt  10421  flqdiv  10430  modqlt  10442  modqdiffl  10444  modqcyc2  10469  modqaddabs  10471  mulqaddmodid  10473  mulp1mod1  10474  modqmuladd  10475  modqmuladdnn0  10477  qnegmod  10478  addmodid  10481  addmodidr  10482  modqadd2mod  10483  modqm1p1mod0  10484  modqmul12d  10487  modqnegd  10488  modqadd12d  10489  modqsub12d  10490  q2submod  10494  modqmulmodr  10499  modqaddmulmod  10500  modqsubdir  10502  modfzo0difsn  10504  modsumfzodifsn  10505  addmodlteq  10507  frecuzrdgsuc  10523  frecfzennn  10535  iseqovex  10567  seq3-1p  10599  seq3caopr2  10602  seqcaopr2g  10603  seq3caopr  10604  seqcaoprg  10605  seqf1oglem2a  10627  seqf1oglem1  10628  seqf1oglem2  10629  seq3id  10634  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  expp1  10655  exprecap  10689  expaddzaplem  10691  expmulzap  10694  expdivap  10699  sqval  10706  sqsubswap  10708  sqdividap  10713  subsq  10755  subsq2  10756  binom2  10760  binom2sub  10762  mulbinom2  10765  binom3  10766  zesq  10767  bernneq2  10770  modqexp  10775  sqoddm1div8  10802  mulsubdivbinom2ap  10820  nn0opthlem1d  10829  nn0opthd  10831  nn0opth2d  10832  facp1  10839  facdiv  10847  facndiv  10848  faclbnd  10850  faclbnd2  10851  faclbnd3  10852  bcval  10858  bccmpl  10863  bcm1k  10869  bcp1n  10870  bcp1nk  10871  bcval5  10872  bcp1m1  10874  bcpasc  10875  bcn2m1  10878  hashprg  10917  hashdifpr  10929  hashfzo  10931  hashfzp1  10933  hashfz0  10934  hashxp  10935  zfz1isolemsplit  10947  zfz1isolem1  10949  seq3coll  10951  reval  11031  crre  11039  remim  11042  remul2  11055  immul2  11062  imval2  11076  cjdivap  11091  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemp1rp  11188  resqrexlemfp1  11191  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  resqrexlemsqa  11206  resqrexlemex  11207  resqrex  11208  sqrtdiv  11224  absvalsq  11235  absreimsq  11249  absdivap  11252  cau3lem  11296  maxabslemlub  11389  maxabslemval  11390  max0addsup  11401  minabs  11418  bdtrilem  11421  bdtri  11422  xrmaxaddlem  11442  xrmaxadd  11443  xrbdtri  11458  clim  11463  clim2  11465  climshftlemg  11484  climshft2  11488  climcn1  11490  climcn2  11491  subcn2  11493  reccn2ap  11495  climmulc2  11513  climsubc2  11515  clim2ser  11519  iser3shft  11528  climcau  11529  serf0  11534  fzosump1  11599  fsum1p  11600  fsump1  11602  sumsplitdc  11614  fsump1i  11615  mptfzshft  11624  fisum0diag2  11629  fsumconst  11636  fsumdifsnconst  11637  modfsummodlemstep  11639  modfsummod  11640  telfsumo  11648  fsumparts  11652  fsumrelem  11653  hash2iun1dif1  11662  binomlem  11665  binom  11666  binom1p  11667  binom1dif  11669  bcxmas  11671  isumsplit  11673  isum1p  11674  arisum  11680  arisum2  11681  trireciplem  11682  geoserap  11689  geolim  11693  geolim2  11694  georeclim  11695  geo2sum  11696  geoisum1  11701  cvgratnnlemseq  11708  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  fprod1p  11781  fprodp1  11782  fprodcl2lem  11787  fprodfac  11797  fprodeq0  11799  fprodconst  11802  fprodrec  11811  fprodsplit1f  11816  fprodmodd  11823  efcllemp  11840  ef0lem  11842  efval  11843  esum  11844  ege2le3  11853  efaddlem  11856  efsep  11873  effsumlt  11874  eft0val  11875  efgt1p2  11877  efgt1p  11878  sinval  11884  cosval  11885  resinval  11897  recosval  11898  efi4p  11899  resin4p  11900  recos4p  11901  sinneg  11908  cosneg  11909  efival  11914  sinadd  11918  cosadd  11919  tanaddap  11921  sinmul  11926  cosmul  11927  cos2t  11932  cos2tsin  11933  ef01bndlem  11938  absefib  11953  demoivre  11955  demoivreALT  11956  eirraplem  11959  p1modz1  11976  dvdsmodexp  11977  moddvds  11981  mulmoddvds  12045  3dvds2dec  12048  zeo3  12050  odd2np1lem  12054  odd2np1  12055  oexpneg  12059  2tp1odd  12066  ltoddhalfle  12075  opoe  12077  opeo  12079  omeo  12080  m1expo  12082  m1exp1  12083  nn0o1gt2  12087  nn0o  12089  divalglemnn  12100  divalglemqt  12101  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  flodddiv4  12118  flodddiv4t2lthalf  12121  bitsp1o  12135  bitsmod  12138  bitsinv1lem  12143  gcdaddm  12176  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  bezoutlemex  12193  bezoutlemaz  12195  mulgcd  12208  gcddiv  12211  gcdmultiplez  12213  rpmulgcd  12218  rplpwr  12219  uzwodc  12229  lcmgcdlem  12270  lcmgcd  12271  divgcdcoprmex  12295  cncongr2  12297  prmexpb  12344  rpexp  12346  rpexp1i  12347  sqrt2irrlem  12354  oddpwdclemxy  12362  oddpwdclemndvds  12364  sqpweven  12368  2sqpwodd  12369  sqne2sq  12370  qmuldeneqnum  12388  nn0gcdsq  12393  zgcdsq  12394  numdensq  12395  dfphi2  12413  phiprmpw  12415  phiprm  12416  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  fermltl  12427  prmdiv  12428  prmdiveq  12429  prmdivdiv  12430  hashgcdlem  12431  odzval  12435  odzcllem  12436  odzdvds  12439  vfermltl  12445  powm2modprm  12446  reumodprminv  12447  modprm0  12448  nnnn0modprm0  12449  modprmn0modprm0  12450  coprimeprodsq  12451  coprimeprodsq2  12452  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  pythagtriplem18  12475  pceu  12489  pczpre  12491  pcdiv  12496  pcqdiv  12501  pcrec  12502  pczndvds  12510  pcneg  12519  pc2dvds  12524  pcprmpw2  12527  pcaddlem  12533  pcadd  12534  fldivp1  12542  pockthlem  12550  pockthi  12552  4sqlem5  12576  4sqlem9  12580  4sqlem10  12581  4sqlem2  12583  4sqlem3  12584  4sqlem4  12586  mul4sqlem  12587  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  4sqlem15  12599  4sqlem17  12601  4sqlem19  12603  ennnfonelemkh  12654  ennnfonelemhf1o  12655  setscomd  12744  ressressg  12778  qusex  13027  qusin  13028  grpinvalem  13087  grpinva  13088  grprida  13089  gsumsplit1r  13100  isnsgrp  13108  sgrpass  13110  sgrp1  13113  sgrppropd  13115  prdssgrpd  13117  mnd12g  13130  mndpropd  13142  prdsidlem  13149  prdsmndd  13150  imasmnd2  13154  mhmex  13164  mhmlin  13169  grprcan  13239  grpinvid1  13254  isgrpinv  13256  grplcan  13264  grpasscan1  13265  grplmulf1o  13276  grpinvadd  13280  grpinvsub  13284  grpsubsub4  13295  grppnpcan2  13296  grpnpncan  13297  dfgrp3mlem  13300  dfgrp3m  13301  grplactcnv  13304  prdsinvlem  13310  imasgrp2  13316  mhmlem  13320  mhmid  13321  mhmmnd  13322  mulgnnp1  13336  mulg2  13337  mulgnn0p1  13339  mulgsubcl  13342  mulgneg  13346  mulgaddcomlem  13351  mulgaddcom  13352  mulgz  13356  mulgnn0dir  13358  mulgdirlem  13359  mulgdir  13360  mulgneg2  13362  mulgnnass  13363  mulgnn0ass  13364  mulgass  13365  mulgassr  13366  mulgmodid  13367  mulgsubdir  13368  submmulg  13372  isnsg3  13413  nmzsubg  13416  ssnmz  13417  0nsg  13420  eqger  13430  eqgid  13432  eqgcpbl  13434  ghmlin  13454  ghmmulg  13462  ghmnsgima  13474  ghmnsgpreima  13475  conjghm  13482  conjnmz  13485  ablsub2inv  13517  abladdsub4  13520  abladdsub  13521  ablpncan2  13522  ablpnpcan  13526  ablnncan  13527  ablnnncan1  13530  gsumfzconst  13547  gsumfzsnfd  13551  mgpress  13563  rngass  13571  rngdi  13572  rngdir  13573  rnglz  13577  rngmneg1  13579  rngsubdir  13584  rngpropd  13587  imasrng  13588  srgass  13603  srgmulgass  13621  srgpcomp  13622  srgpcompp  13623  srgpcomppsc  13624  ringpropd  13670  ringlz  13675  ring1eq0  13680  ringnegl  13683  ringmneg1  13685  ringsubdir  13689  mulgass2  13690  ring1  13691  imasring  13696  opprrng  13709  opprring  13711  unitgrp  13748  dvrcan1  13772  rdivmuldivd  13776  subrginv  13869  resrhm  13880  unitrrg  13899  islmod  13923  lmodlema  13924  islmodd  13925  lmod0vs  13953  lmodvs0  13954  lmodvsmmulgdi  13955  lmodvneg1  13962  lmodvsneg  13963  lmodsubvs  13975  lmodsubdi  13976  lmodsubdir  13977  lmodprop2d  13980  rmodislmodlem  13982  rmodislmod  13983  lsssetm  13988  islssmd  13991  lssclg  13996  lssvacl  13997  lss1d  14015  lsspropdg  14063  sraval  14069  rnglidlmcl  14112  gsumfzfsumlemm  14219  znunit  14291  resttop  14490  restco  14494  restin  14496  lmfval  14512  cnprcl2k  14526  txrest  14596  txdis1cn  14598  cnmpt2res  14617  psmettri2  14648  psmettri  14650  xmettri2  14681  xmettri  14692  mettri  14693  metrtri  14697  blvalps  14708  blval  14709  xblss2  14725  blhalf  14728  comet  14819  xmetxp  14827  txmetcnp  14838  cnmet  14850  ioo2bl  14871  ivthreinc  14965  limcmpted  14983  limcimolemlt  14984  cnplimclemr  14989  limccnp2cntop  14997  reldvg  14999  dvfvalap  15001  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvconst  15014  dvconstre  15016  dvconstss  15018  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvexp  15031  dvrecap  15033  dvmptcmulcn  15041  dveflem  15046  plyval  15052  elply2  15055  elplyr  15060  elplyd  15061  ply1termlem  15062  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plycjlemc  15080  dvply1  15085  sin0pilem1  15101  sinperlem  15128  ptolemy  15144  tangtx  15158  abssinper  15166  reexplog  15191  relogexp  15192  cxprec  15230  rpdivcxp  15231  cxpmul  15232  rpabscxpbnd  15260  rplogbval  15265  rplogbreexp  15273  rprelogbmul  15275  logbrec  15280  logbgcd1irraplemap  15289  binom4  15299  wilthlem1  15300  mpodvdsmulf1o  15310  sgmppw  15312  0sgmppw  15313  1sgmprm  15314  1sgm2ppw  15315  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgslem1  15325  lgslem4  15328  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsval4lem  15336  lgsvalmod  15344  lgsneg  15349  lgsneg1  15350  lgsmod  15351  lgsdilem  15352  lgsdir2lem4  15356  lgsdir2  15358  lgsdirprm  15359  lgsdir  15360  lgsne0  15363  lgssq  15365  lgssq2  15366  lgsmulsqcoprm  15371  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  gausslemma2dlem5a  15390  gausslemma2dlem5  15391  gausslemma2dlem6  15392  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  lgsquad2lem2  15407  lgsquad3  15409  m1lgs  15410  2lgslem1a  15413  2lgslem1c  15415  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgsoddprmlem1  15430  2lgsoddprmlem2  15431  2lgsoddprmlem3  15436  2sqlem1  15439  2sqlem2  15440  mul2sq  15441  2sqlem3  15442  2sqlem4  15443  2sqlem8  15448  2sqlem9  15449  2sqlem10  15450  trilpolemeq1  15771  trilpolemlt1  15772  trirec0xor  15776  apdifflemf  15777  apdiff  15779