Theorem oveq1d 5840

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 5832	. 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 1335  (class class class)co 5825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-br 3967  df-iota 5136  df-fv 5179  df-ov 5828

This theorem is referenced by:  fvoveq1d  5847  csbov2g  5863  caovassg  5980  caovdig  5996  caovdirg  5999  caov12d  6003  caov31d  6004  caov411d  6007  grprinvlem  6016  grprinvd  6017  grpridd  6018  caofinvl  6055  omsuc  6420  nnmsucr  6436  nnm1  6472  nnm2  6473  ecovass  6590  ecoviass  6591  ecovdi  6592  ecovidi  6593  addasspig  7251  mulasspig  7253  mulpipq2  7292  distrnqg  7308  ltsonq  7319  ltanqg  7321  ltmnqg  7322  ltexnqq  7329  archnqq  7338  prarloclemarch2  7340  enq0sym  7353  addnq0mo  7368  mulnq0mo  7369  addnnnq0  7370  nqpnq0nq  7374  nq0m0r  7377  nq0a0  7378  nnanq0  7379  distrnq0  7380  addassnq0  7383  addpinq1  7385  prarloclemlo  7415  prarloclem3  7418  prarloclem5  7421  prarloclemcalc  7423  addnqprllem  7448  addnqprulem  7449  appdivnq  7484  recexprlem1ssl  7554  recexprlem1ssu  7555  ltmprr  7563  cauappcvgprlemladdru  7577  cauappcvgprlem1  7580  caucvgprlemnkj  7587  caucvgprlemnbj  7588  caucvgprlemcl  7597  caucvgprlemladdfu  7598  caucvgprlemladdrl  7599  caucvgprlem1  7600  caucvgprprlemcbv  7608  caucvgprprlemval  7609  caucvgprprlemexb  7628  caucvgprprlem1  7630  addcmpblnr  7660  mulcmpblnrlemg  7661  addsrmo  7664  mulsrmo  7665  addsrpr  7666  mulsrpr  7667  ltsrprg  7668  1idsr  7689  pn0sr  7692  recexgt0sr  7694  mulgt0sr  7699  srpospr  7704  prsradd  7707  caucvgsrlemfv  7712  caucvgsrlemcau  7714  caucvgsrlemgt1  7716  caucvgsrlemoffval  7717  caucvgsrlemoffcau  7719  caucvgsrlemoffres  7721  caucvgsrlembnd  7722  caucvgsr  7723  map2psrprg  7726  pitonnlem1p1  7767  pitonnlem2  7768  pitonn  7769  recidpirqlemcalc  7778  ax1rid  7798  axrnegex  7800  axcnre  7802  recriota  7811  nntopi  7815  axcaucvglemval  7818  axcaucvglemcau  7819  axcaucvglemres  7820  mul12  8005  mul4  8008  muladd11  8009  readdcan  8016  muladd11r  8032  add12  8034  cnegex  8054  addcan  8056  negeu  8067  pncan2  8083  addsubass  8086  addsub  8087  2addsub  8090  addsubeq4  8091  subid  8095  subid1  8096  npncan  8097  nppcan  8098  nnpcan  8099  nnncan1  8112  npncan3  8114  pnpcan  8115  pnncan  8117  ppncan  8118  addsub4  8119  negsub  8124  subneg  8125  subeqxfrd  8239  mvlraddd  8240  mvlladdd  8241  mvrraddd  8242  subaddeqd  8245  ine0  8270  mulneg1  8271  ltadd2  8295  apreap  8463  cru  8478  recexap  8528  mulcanapd  8536  div23ap  8565  div13ap  8567  divmulassap  8569  divmulasscomap  8570  divcanap4  8573  muldivdirap  8581  divsubdirap  8582  divmuldivap  8586  divdivdivap  8587  divcanap5  8588  divmul13ap  8589  divmuleqap  8591  divdiv32ap  8594  divcanap7  8595  dmdcanap  8596  divdivap1  8597  divdivap2  8598  divadddivap  8601  divsubdivap  8602  conjmulap  8603  divneg2ap  8610  subrecap  8712  mvllmulapd  8715  lt2mul2div  8751  nndivtr  8876  2halves  9063  halfaddsub  9068  avgle1  9074  avgle2  9075  div4p1lem1div2  9087  un0addcl  9124  un0mulcl  9125  peano2z  9204  zneo  9266  nneoor  9267  nneo  9268  zeo  9270  zeo2  9271  deceq1  9300  qreccl  9552  xaddcom  9766  xnegdi  9773  xaddass  9774  xaddass2  9775  xpncan  9776  xleadd1a  9778  xltadd1  9781  xposdif  9787  xadd4d  9790  lincmb01cmp  9908  iccf1o  9909  fz0to4untppr  10027  fzosubel3  10099  qavgle  10162  2tnp1ge0ge0  10204  fldiv4p1lem1div2  10208  ceilqm1lt  10215  flqdiv  10224  modqlt  10236  modqdiffl  10238  modqcyc2  10263  modqaddabs  10265  mulqaddmodid  10267  mulp1mod1  10268  modqmuladd  10269  modqmuladdnn0  10271  qnegmod  10272  addmodid  10275  addmodidr  10276  modqadd2mod  10277  modqm1p1mod0  10278  modqmul12d  10281  modqnegd  10282  modqadd12d  10283  modqsub12d  10284  q2submod  10288  modqmulmodr  10293  modqaddmulmod  10294  modqsubdir  10296  modfzo0difsn  10298  modsumfzodifsn  10299  addmodlteq  10301  frecuzrdgsuc  10317  frecfzennn  10329  iseqovex  10359  seq3-1p  10383  seq3caopr2  10385  seq3caopr  10386  seq3id  10411  seq3homo  10413  seq3z  10414  expp1  10430  exprecap  10464  expaddzaplem  10466  expmulzap  10469  expdivap  10474  sqval  10481  sqsubswap  10483  subsq  10529  subsq2  10530  binom2  10533  binom2sub  10535  mulbinom2  10538  binom3  10539  zesq  10540  bernneq2  10543  modqexp  10548  sqoddm1div8  10575  nn0opthlem1d  10598  nn0opthd  10600  nn0opth2d  10601  facp1  10608  facdiv  10616  facndiv  10617  faclbnd  10619  faclbnd2  10620  faclbnd3  10621  bcval  10627  bccmpl  10632  bcm1k  10638  bcp1n  10639  bcp1nk  10640  bcval5  10641  bcp1m1  10643  bcpasc  10644  bcn2m1  10647  hashprg  10686  hashdifpr  10698  hashfzo  10700  hashfzp1  10702  hashfz0  10703  hashxp  10704  zfz1isolemsplit  10713  zfz1isolem1  10715  seq3coll  10717  reval  10753  crre  10761  remim  10764  remul2  10777  immul2  10784  imval2  10798  cjdivap  10813  caucvgre  10885  cvg1nlemcau  10888  cvg1nlemres  10889  resqrexlemp1rp  10910  resqrexlemfp1  10913  resqrexlemover  10914  resqrexlemcalc1  10918  resqrexlemcalc3  10920  resqrexlemnm  10922  resqrexlemoverl  10925  resqrexlemglsq  10926  resqrexlemga  10927  resqrexlemsqa  10928  resqrexlemex  10929  resqrex  10930  sqrtdiv  10946  absvalsq  10957  absreimsq  10971  absdivap  10974  cau3lem  11018  maxabslemlub  11111  maxabslemval  11112  max0addsup  11123  minabs  11139  bdtrilem  11142  bdtri  11143  xrmaxaddlem  11161  xrmaxadd  11162  xrbdtri  11177  clim  11182  clim2  11184  climshftlemg  11203  climshft2  11207  climcn1  11209  climcn2  11210  subcn2  11212  reccn2ap  11214  climmulc2  11232  climsubc2  11234  clim2ser  11238  iser3shft  11247  climcau  11248  serf0  11253  fzosump1  11318  fsum1p  11319  fsump1  11321  sumsplitdc  11333  fsump1i  11334  mptfzshft  11343  fisum0diag2  11348  fsumconst  11355  fsumdifsnconst  11356  modfsummodlemstep  11358  modfsummod  11359  telfsumo  11367  fsumparts  11371  fsumrelem  11372  hash2iun1dif1  11381  binomlem  11384  binom  11385  binom1p  11386  binom1dif  11388  bcxmas  11390  isumsplit  11392  isum1p  11393  arisum  11399  arisum2  11400  trireciplem  11401  geoserap  11408  geolim  11412  geolim2  11413  georeclim  11414  geo2sum  11415  geoisum1  11420  cvgratnnlemseq  11427  cvgratnnlemsumlt  11429  cvgratnnlemfm  11430  cvgratz  11433  mertenslemi1  11436  mertenslem2  11437  mertensabs  11438  fprod1p  11500  fprodp1  11501  fprodcl2lem  11506  fprodfac  11516  fprodeq0  11518  fprodconst  11521  fprodrec  11530  fprodsplit1f  11535  fprodmodd  11542  efcllemp  11559  ef0lem  11561  efval  11562  esum  11563  ege2le3  11572  efaddlem  11575  efsep  11592  effsumlt  11593  eft0val  11594  efgt1p2  11596  efgt1p  11597  sinval  11603  cosval  11604  resinval  11616  recosval  11617  efi4p  11618  resin4p  11619  recos4p  11620  sinneg  11627  cosneg  11628  efival  11633  sinadd  11637  cosadd  11638  tanaddap  11640  sinmul  11645  cosmul  11646  cos2t  11651  cos2tsin  11652  ef01bndlem  11657  absefib  11671  demoivre  11673  demoivreALT  11674  eirraplem  11677  p1modz1  11694  dvdsmodexp  11695  moddvds  11699  mulmoddvds  11759  3dvds2dec  11761  zeo3  11763  odd2np1lem  11767  odd2np1  11768  oexpneg  11772  2tp1odd  11779  ltoddhalfle  11788  opoe  11790  opeo  11792  omeo  11793  m1expo  11795  m1exp1  11796  nn0o1gt2  11800  nn0o  11802  divalglemnn  11813  divalglemqt  11814  divalglemeunn  11816  divalglemex  11817  divalglemeuneg  11818  flodddiv4  11829  flodddiv4t2lthalf  11832  gcdaddm  11872  bezoutlemnewy  11884  bezoutlema  11887  bezoutlemb  11888  bezoutlemex  11889  bezoutlemaz  11891  mulgcd  11904  gcddiv  11907  gcdmultiplez  11909  rpmulgcd  11914  rplpwr  11915  lcmgcdlem  11958  lcmgcd  11959  divgcdcoprmex  11983  cncongr2  11985  prmexpb  12030  rpexp  12032  rpexp1i  12033  sqrt2irrlem  12040  oddpwdclemxy  12048  oddpwdclemndvds  12050  sqpweven  12054  2sqpwodd  12055  sqne2sq  12056  qmuldeneqnum  12074  nn0gcdsq  12079  zgcdsq  12080  numdensq  12081  dfphi2  12099  phiprmpw  12101  phiprm  12102  eulerthlema  12109  eulerthlemh  12110  eulerthlemth  12111  fermltl  12113  prmdiv  12114  prmdiveq  12115  prmdivdiv  12116  hashgcdlem  12117  odzval  12120  odzcllem  12121  odzdvds  12124  vfermltl  12130  powm2modprm  12131  reumodprminv  12132  modprm0  12133  nnnn0modprm0  12134  modprmn0modprm0  12135  coprimeprodsq  12136  coprimeprodsq2  12137  pythagtriplem1  12144  pythagtriplem3  12146  pythagtriplem4  12147  pythagtriplem6  12149  pythagtriplem7  12150  pythagtriplem12  12154  pythagtriplem14  12156  pythagtriplem15  12157  pythagtriplem16  12158  pythagtriplem17  12159  pythagtriplem18  12160  ennnfonelemkh  12183  ennnfonelemhf1o  12184  resttop  12612  restco  12616  restin  12618  lmfval  12634  cnprcl2k  12648  txrest  12718  txdis1cn  12720  cnmpt2res  12739  psmettri2  12770  psmettri  12772  xmettri2  12803  xmettri  12814  mettri  12815  metrtri  12819  blvalps  12830  blval  12831  xblss2  12847  blhalf  12850  comet  12941  xmetxp  12949  txmetcnp  12960  cnmet  12972  ioo2bl  12985  limcmpted  13074  limcimolemlt  13075  cnplimclemr  13080  limccnp2cntop  13088  reldvg  13090  dvfvalap  13092  dvidlemap  13102  dvconst  13103  dvcnp2cntop  13105  dvaddxxbr  13107  dvmulxxbr  13108  dvcoapbr  13113  dvcjbr  13114  dvexp  13117  dvrecap  13119  dvmptcmulcn  13125  dveflem  13129  sin0pilem1  13144  sinperlem  13171  ptolemy  13187  tangtx  13201  abssinper  13209  reexplog  13234  relogexp  13235  cxprec  13273  rpdivcxp  13274  cxpmul  13275  rpabscxpbnd  13301  rplogbval  13304  rplogbreexp  13312  rprelogbmul  13314  logbrec  13319  logbgcd1irraplemap  13328  binom4  13338  trilpolemeq1  13653  trilpolemlt1  13654  trirec0xor  13658  apdifflemf  13659  apdiff  13661