Theorem oveq1d 5856

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 5848	. 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 1343  (class class class)co 5841

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  fvoveq1d  5863  csbov2g  5879  caovassg  5996  caovdig  6012  caovdirg  6015  caov12d  6019  caov31d  6020  caov411d  6023  grprinvlem  6032  grprinvd  6033  grpridd  6034  caofinvl  6071  omsuc  6436  nnmsucr  6452  nnm1  6488  nnm2  6489  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  addasspig  7267  mulasspig  7269  mulpipq2  7308  distrnqg  7324  ltsonq  7335  ltanqg  7337  ltmnqg  7338  ltexnqq  7345  archnqq  7354  prarloclemarch2  7356  enq0sym  7369  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  nqpnq0nq  7390  nq0m0r  7393  nq0a0  7394  nnanq0  7395  distrnq0  7396  addassnq0  7399  addpinq1  7401  prarloclemlo  7431  prarloclem3  7434  prarloclem5  7437  prarloclemcalc  7439  addnqprllem  7464  addnqprulem  7465  appdivnq  7500  recexprlem1ssl  7570  recexprlem1ssu  7571  ltmprr  7579  cauappcvgprlemladdru  7593  cauappcvgprlem1  7596  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemexb  7644  caucvgprprlem1  7646  addcmpblnr  7676  mulcmpblnrlemg  7677  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  ltsrprg  7684  1idsr  7705  pn0sr  7708  recexgt0sr  7710  mulgt0sr  7715  srpospr  7720  prsradd  7723  caucvgsrlemfv  7728  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffval  7733  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  caucvgsrlembnd  7738  caucvgsr  7739  map2psrprg  7742  pitonnlem1p1  7783  pitonnlem2  7784  pitonn  7785  recidpirqlemcalc  7794  ax1rid  7814  axrnegex  7816  axcnre  7818  recriota  7827  nntopi  7831  axcaucvglemval  7834  axcaucvglemcau  7835  axcaucvglemres  7836  mul12  8023  mul4  8026  muladd11  8027  readdcan  8034  muladd11r  8050  add12  8052  cnegex  8072  addcan  8074  negeu  8085  pncan2  8101  addsubass  8104  addsub  8105  2addsub  8108  addsubeq4  8109  subid  8113  subid1  8114  npncan  8115  nppcan  8116  nnpcan  8117  nnncan1  8130  npncan3  8132  pnpcan  8133  pnncan  8135  ppncan  8136  addsub4  8137  negsub  8142  subneg  8143  subeqxfrd  8257  mvlraddd  8258  mvlladdd  8259  mvrraddd  8260  subaddeqd  8263  ine0  8288  mulneg1  8289  ltadd2  8313  apreap  8481  cru  8496  recexap  8546  mulcanapd  8554  div23ap  8583  div13ap  8585  divmulassap  8587  divmulasscomap  8588  divcanap4  8591  muldivdirap  8599  divsubdirap  8600  divmuldivap  8604  divdivdivap  8605  divcanap5  8606  divmul13ap  8607  divmuleqap  8609  divdiv32ap  8612  divcanap7  8613  dmdcanap  8614  divdivap1  8615  divdivap2  8616  divadddivap  8619  divsubdivap  8620  conjmulap  8621  divneg2ap  8628  subrecap  8731  mvllmulapd  8734  lt2mul2div  8770  nndivtr  8895  2halves  9082  halfaddsub  9087  avgle1  9093  avgle2  9094  div4p1lem1div2  9106  un0addcl  9143  un0mulcl  9144  peano2z  9223  zneo  9288  nneoor  9289  nneo  9290  zeo  9292  zeo2  9293  deceq1  9322  qreccl  9576  xaddcom  9793  xnegdi  9800  xaddass  9801  xaddass2  9802  xpncan  9803  xleadd1a  9805  xltadd1  9808  xposdif  9814  xadd4d  9817  lincmb01cmp  9935  iccf1o  9936  fz0to4untppr  10055  fzosubel3  10127  qavgle  10190  2tnp1ge0ge0  10232  fldiv4p1lem1div2  10236  ceilqm1lt  10243  flqdiv  10252  modqlt  10264  modqdiffl  10266  modqcyc2  10291  modqaddabs  10293  mulqaddmodid  10295  mulp1mod1  10296  modqmuladd  10297  modqmuladdnn0  10299  qnegmod  10300  addmodid  10303  addmodidr  10304  modqadd2mod  10305  modqm1p1mod0  10306  modqmul12d  10309  modqnegd  10310  modqadd12d  10311  modqsub12d  10312  q2submod  10316  modqmulmodr  10321  modqaddmulmod  10322  modqsubdir  10324  modfzo0difsn  10326  modsumfzodifsn  10327  addmodlteq  10329  frecuzrdgsuc  10345  frecfzennn  10357  iseqovex  10387  seq3-1p  10411  seq3caopr2  10413  seq3caopr  10414  seq3id  10439  seq3homo  10441  seq3z  10442  expp1  10458  exprecap  10492  expaddzaplem  10494  expmulzap  10497  expdivap  10502  sqval  10509  sqsubswap  10511  subsq  10557  subsq2  10558  binom2  10562  binom2sub  10564  mulbinom2  10567  binom3  10568  zesq  10569  bernneq2  10572  modqexp  10577  sqoddm1div8  10604  nn0opthlem1d  10629  nn0opthd  10631  nn0opth2d  10632  facp1  10639  facdiv  10647  facndiv  10648  faclbnd  10650  faclbnd2  10651  faclbnd3  10652  bcval  10658  bccmpl  10663  bcm1k  10669  bcp1n  10670  bcp1nk  10671  bcval5  10672  bcp1m1  10674  bcpasc  10675  bcn2m1  10678  hashprg  10717  hashdifpr  10729  hashfzo  10731  hashfzp1  10733  hashfz0  10734  hashxp  10735  zfz1isolemsplit  10747  zfz1isolem1  10749  seq3coll  10751  reval  10787  crre  10795  remim  10798  remul2  10811  immul2  10818  imval2  10832  cjdivap  10847  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  resqrexlemsqa  10962  resqrexlemex  10963  resqrex  10964  sqrtdiv  10980  absvalsq  10991  absreimsq  11005  absdivap  11008  cau3lem  11052  maxabslemlub  11145  maxabslemval  11146  max0addsup  11157  minabs  11173  bdtrilem  11176  bdtri  11177  xrmaxaddlem  11197  xrmaxadd  11198  xrbdtri  11213  clim  11218  clim2  11220  climshftlemg  11239  climshft2  11243  climcn1  11245  climcn2  11246  subcn2  11248  reccn2ap  11250  climmulc2  11268  climsubc2  11270  clim2ser  11274  iser3shft  11283  climcau  11284  serf0  11289  fzosump1  11354  fsum1p  11355  fsump1  11357  sumsplitdc  11369  fsump1i  11370  mptfzshft  11379  fisum0diag2  11384  fsumconst  11391  fsumdifsnconst  11392  modfsummodlemstep  11394  modfsummod  11395  telfsumo  11403  fsumparts  11407  fsumrelem  11408  hash2iun1dif1  11417  binomlem  11420  binom  11421  binom1p  11422  binom1dif  11424  bcxmas  11426  isumsplit  11428  isum1p  11429  arisum  11435  arisum2  11436  trireciplem  11437  geoserap  11444  geolim  11448  geolim2  11449  georeclim  11450  geo2sum  11451  geoisum1  11456  cvgratnnlemseq  11463  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  fprod1p  11536  fprodp1  11537  fprodcl2lem  11542  fprodfac  11552  fprodeq0  11554  fprodconst  11557  fprodrec  11566  fprodsplit1f  11571  fprodmodd  11578  efcllemp  11595  ef0lem  11597  efval  11598  esum  11599  ege2le3  11608  efaddlem  11611  efsep  11628  effsumlt  11629  eft0val  11630  efgt1p2  11632  efgt1p  11633  sinval  11639  cosval  11640  resinval  11652  recosval  11653  efi4p  11654  resin4p  11655  recos4p  11656  sinneg  11663  cosneg  11664  efival  11669  sinadd  11673  cosadd  11674  tanaddap  11676  sinmul  11681  cosmul  11682  cos2t  11687  cos2tsin  11688  ef01bndlem  11693  absefib  11707  demoivre  11709  demoivreALT  11710  eirraplem  11713  p1modz1  11730  dvdsmodexp  11731  moddvds  11735  mulmoddvds  11797  3dvds2dec  11799  zeo3  11801  odd2np1lem  11805  odd2np1  11806  oexpneg  11810  2tp1odd  11817  ltoddhalfle  11826  opoe  11828  opeo  11830  omeo  11831  m1expo  11833  m1exp1  11834  nn0o1gt2  11838  nn0o  11840  divalglemnn  11851  divalglemqt  11852  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  flodddiv4  11867  flodddiv4t2lthalf  11870  gcdaddm  11913  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  bezoutlemex  11930  bezoutlemaz  11932  mulgcd  11945  gcddiv  11948  gcdmultiplez  11950  rpmulgcd  11955  rplpwr  11956  uzwodc  11966  lcmgcdlem  12005  lcmgcd  12006  divgcdcoprmex  12030  cncongr2  12032  prmexpb  12079  rpexp  12081  rpexp1i  12082  sqrt2irrlem  12089  oddpwdclemxy  12097  oddpwdclemndvds  12099  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  qmuldeneqnum  12123  nn0gcdsq  12128  zgcdsq  12129  numdensq  12130  dfphi2  12148  phiprmpw  12150  phiprm  12151  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  fermltl  12162  prmdiv  12163  prmdiveq  12164  prmdivdiv  12165  hashgcdlem  12166  odzval  12169  odzcllem  12170  odzdvds  12173  vfermltl  12179  powm2modprm  12180  reumodprminv  12181  modprm0  12182  nnnn0modprm0  12183  modprmn0modprm0  12184  coprimeprodsq  12185  coprimeprodsq2  12186  pythagtriplem1  12193  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  pythagtriplem18  12209  pceu  12223  pczpre  12225  pcdiv  12230  pcqdiv  12235  pcrec  12236  pczndvds  12243  pcneg  12252  pc2dvds  12257  pcprmpw2  12260  pcaddlem  12266  pcadd  12267  fldivp1  12274  pockthlem  12282  pockthi  12284  4sqlem5  12308  4sqlem9  12312  4sqlem10  12313  4sqlem2  12315  4sqlem3  12316  4sqlem4  12318  mul4sqlem  12319  ennnfonelemkh  12341  ennnfonelemhf1o  12342  resttop  12770  restco  12774  restin  12776  lmfval  12792  cnprcl2k  12806  txrest  12876  txdis1cn  12878  cnmpt2res  12897  psmettri2  12928  psmettri  12930  xmettri2  12961  xmettri  12972  mettri  12973  metrtri  12977  blvalps  12988  blval  12989  xblss2  13005  blhalf  13008  comet  13099  xmetxp  13107  txmetcnp  13118  cnmet  13130  ioo2bl  13143  limcmpted  13232  limcimolemlt  13233  cnplimclemr  13238  limccnp2cntop  13246  reldvg  13248  dvfvalap  13250  dvidlemap  13260  dvconst  13261  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvexp  13275  dvrecap  13277  dvmptcmulcn  13283  dveflem  13287  sin0pilem1  13302  sinperlem  13329  ptolemy  13345  tangtx  13359  abssinper  13367  reexplog  13392  relogexp  13393  cxprec  13431  rpdivcxp  13432  cxpmul  13433  rpabscxpbnd  13459  rplogbval  13463  rplogbreexp  13471  rprelogbmul  13473  logbrec  13478  logbgcd1irraplemap  13487  binom4  13497  lgslem1  13501  lgslem4  13504  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsval4lem  13512  lgsvalmod  13520  lgsneg  13525  lgsneg1  13526  lgsmod  13527  lgsdilem  13528  lgsdir2lem4  13532  lgsdir2  13534  lgsdirprm  13535  lgsdir  13536  lgsne0  13539  lgssq  13541  lgssq2  13542  lgsmulsqcoprm  13547  lgsdirnn0  13548  lgsdinn0  13549  2sqlem1  13550  2sqlem2  13551  mul2sq  13552  2sqlem3  13553  2sqlem4  13554  2sqlem8  13559  2sqlem9  13560  2sqlem10  13561  trilpolemeq1  13879  trilpolemlt1  13880  trirec0xor  13884  apdifflemf  13885  apdiff  13887