Theorem oveq1d 5893

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 5885	. 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 1353  (class class class)co 5878

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5881

This theorem is referenced by:  fvoveq1d  5900  csbov2g  5919  caovassg  6036  caovdig  6052  caovdirg  6055  caov12d  6059  caov31d  6060  caov411d  6063  caofinvl  6108  omsuc  6476  nnmsucr  6492  nnm1  6529  nnm2  6530  ecovass  6647  ecoviass  6648  ecovdi  6649  ecovidi  6650  addasspig  7332  mulasspig  7334  mulpipq2  7373  distrnqg  7389  ltsonq  7400  ltanqg  7402  ltmnqg  7403  ltexnqq  7410  archnqq  7419  prarloclemarch2  7421  enq0sym  7434  addnq0mo  7449  mulnq0mo  7450  addnnnq0  7451  nqpnq0nq  7455  nq0m0r  7458  nq0a0  7459  nnanq0  7460  distrnq0  7461  addassnq0  7464  addpinq1  7466  prarloclemlo  7496  prarloclem3  7499  prarloclem5  7502  prarloclemcalc  7504  addnqprllem  7529  addnqprulem  7530  appdivnq  7565  recexprlem1ssl  7635  recexprlem1ssu  7636  ltmprr  7644  cauappcvgprlemladdru  7658  cauappcvgprlem1  7661  caucvgprlemnkj  7668  caucvgprlemnbj  7669  caucvgprlemcl  7678  caucvgprlemladdfu  7679  caucvgprlemladdrl  7680  caucvgprlem1  7681  caucvgprprlemcbv  7689  caucvgprprlemval  7690  caucvgprprlemexb  7709  caucvgprprlem1  7711  addcmpblnr  7741  mulcmpblnrlemg  7742  addsrmo  7745  mulsrmo  7746  addsrpr  7747  mulsrpr  7748  ltsrprg  7749  1idsr  7770  pn0sr  7773  recexgt0sr  7775  mulgt0sr  7780  srpospr  7785  prsradd  7788  caucvgsrlemfv  7793  caucvgsrlemcau  7795  caucvgsrlemgt1  7797  caucvgsrlemoffval  7798  caucvgsrlemoffcau  7800  caucvgsrlemoffres  7802  caucvgsrlembnd  7803  caucvgsr  7804  map2psrprg  7807  pitonnlem1p1  7848  pitonnlem2  7849  pitonn  7850  recidpirqlemcalc  7859  ax1rid  7879  axrnegex  7881  axcnre  7883  recriota  7892  nntopi  7896  axcaucvglemval  7899  axcaucvglemcau  7900  axcaucvglemres  7901  mul12  8089  mul4  8092  muladd11  8093  readdcan  8100  muladd11r  8116  add12  8118  cnegex  8138  addcan  8140  negeu  8151  pncan2  8167  addsubass  8170  addsub  8171  2addsub  8174  addsubeq4  8175  subid  8179  subid1  8180  npncan  8181  nppcan  8182  nnpcan  8183  nnncan1  8196  npncan3  8198  pnpcan  8199  pnncan  8201  ppncan  8202  addsub4  8203  negsub  8208  subneg  8209  subeqxfrd  8323  mvlraddd  8324  mvlladdd  8325  mvrraddd  8326  subaddeqd  8329  ine0  8354  mulneg1  8355  ltadd2  8379  apreap  8547  cru  8562  recexap  8613  mulcanapd  8621  div23ap  8651  div13ap  8653  divmulassap  8655  divmulasscomap  8656  divcanap4  8659  muldivdirap  8667  divsubdirap  8668  divmuldivap  8672  divdivdivap  8673  divcanap5  8674  divmul13ap  8675  divmuleqap  8677  divdiv32ap  8680  divcanap7  8681  dmdcanap  8682  divdivap1  8683  divdivap2  8684  divadddivap  8687  divsubdivap  8688  conjmulap  8689  divneg2ap  8696  subrecap  8799  mvllmulapd  8802  lt2mul2div  8839  nndivtr  8964  2halves  9151  halfaddsub  9156  avgle1  9162  avgle2  9163  div4p1lem1div2  9175  un0addcl  9212  un0mulcl  9213  peano2z  9292  zneo  9357  nneoor  9358  nneo  9359  zeo  9361  zeo2  9362  deceq1  9391  qreccl  9645  xaddcom  9864  xnegdi  9871  xaddass  9872  xaddass2  9873  xpncan  9874  xleadd1a  9876  xltadd1  9879  xposdif  9885  xadd4d  9888  lincmb01cmp  10006  iccf1o  10007  fz0to4untppr  10127  fzosubel3  10199  qavgle  10262  2tnp1ge0ge0  10304  fldiv4p1lem1div2  10308  ceilqm1lt  10315  flqdiv  10324  modqlt  10336  modqdiffl  10338  modqcyc2  10363  modqaddabs  10365  mulqaddmodid  10367  mulp1mod1  10368  modqmuladd  10369  modqmuladdnn0  10371  qnegmod  10372  addmodid  10375  addmodidr  10376  modqadd2mod  10377  modqm1p1mod0  10378  modqmul12d  10381  modqnegd  10382  modqadd12d  10383  modqsub12d  10384  q2submod  10388  modqmulmodr  10393  modqaddmulmod  10394  modqsubdir  10396  modfzo0difsn  10398  modsumfzodifsn  10399  addmodlteq  10401  frecuzrdgsuc  10417  frecfzennn  10429  iseqovex  10459  seq3-1p  10483  seq3caopr2  10485  seq3caopr  10486  seq3id  10511  seq3homo  10513  seq3z  10514  expp1  10530  exprecap  10564  expaddzaplem  10566  expmulzap  10569  expdivap  10574  sqval  10581  sqsubswap  10583  sqdividap  10588  subsq  10630  subsq2  10631  binom2  10635  binom2sub  10637  mulbinom2  10640  binom3  10641  zesq  10642  bernneq2  10645  modqexp  10650  sqoddm1div8  10677  mulsubdivbinom2ap  10694  nn0opthlem1d  10703  nn0opthd  10705  nn0opth2d  10706  facp1  10713  facdiv  10721  facndiv  10722  faclbnd  10724  faclbnd2  10725  faclbnd3  10726  bcval  10732  bccmpl  10737  bcm1k  10743  bcp1n  10744  bcp1nk  10745  bcval5  10746  bcp1m1  10748  bcpasc  10749  bcn2m1  10752  hashprg  10791  hashdifpr  10803  hashfzo  10805  hashfzp1  10807  hashfz0  10808  hashxp  10809  zfz1isolemsplit  10821  zfz1isolem1  10823  seq3coll  10825  reval  10861  crre  10869  remim  10872  remul2  10885  immul2  10892  imval2  10906  cjdivap  10921  caucvgre  10993  cvg1nlemcau  10996  cvg1nlemres  10997  resqrexlemp1rp  11018  resqrexlemfp1  11021  resqrexlemover  11022  resqrexlemcalc1  11026  resqrexlemcalc3  11028  resqrexlemnm  11030  resqrexlemoverl  11033  resqrexlemglsq  11034  resqrexlemga  11035  resqrexlemsqa  11036  resqrexlemex  11037  resqrex  11038  sqrtdiv  11054  absvalsq  11065  absreimsq  11079  absdivap  11082  cau3lem  11126  maxabslemlub  11219  maxabslemval  11220  max0addsup  11231  minabs  11247  bdtrilem  11250  bdtri  11251  xrmaxaddlem  11271  xrmaxadd  11272  xrbdtri  11287  clim  11292  clim2  11294  climshftlemg  11313  climshft2  11317  climcn1  11319  climcn2  11320  subcn2  11322  reccn2ap  11324  climmulc2  11342  climsubc2  11344  clim2ser  11348  iser3shft  11357  climcau  11358  serf0  11363  fzosump1  11428  fsum1p  11429  fsump1  11431  sumsplitdc  11443  fsump1i  11444  mptfzshft  11453  fisum0diag2  11458  fsumconst  11465  fsumdifsnconst  11466  modfsummodlemstep  11468  modfsummod  11469  telfsumo  11477  fsumparts  11481  fsumrelem  11482  hash2iun1dif1  11491  binomlem  11494  binom  11495  binom1p  11496  binom1dif  11498  bcxmas  11500  isumsplit  11502  isum1p  11503  arisum  11509  arisum2  11510  trireciplem  11511  geoserap  11518  geolim  11522  geolim2  11523  georeclim  11524  geo2sum  11525  geoisum1  11530  cvgratnnlemseq  11537  cvgratnnlemsumlt  11539  cvgratnnlemfm  11540  cvgratz  11543  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  fprod1p  11610  fprodp1  11611  fprodcl2lem  11616  fprodfac  11626  fprodeq0  11628  fprodconst  11631  fprodrec  11640  fprodsplit1f  11645  fprodmodd  11652  efcllemp  11669  ef0lem  11671  efval  11672  esum  11673  ege2le3  11682  efaddlem  11685  efsep  11702  effsumlt  11703  eft0val  11704  efgt1p2  11706  efgt1p  11707  sinval  11713  cosval  11714  resinval  11726  recosval  11727  efi4p  11728  resin4p  11729  recos4p  11730  sinneg  11737  cosneg  11738  efival  11743  sinadd  11747  cosadd  11748  tanaddap  11750  sinmul  11755  cosmul  11756  cos2t  11761  cos2tsin  11762  ef01bndlem  11767  absefib  11781  demoivre  11783  demoivreALT  11784  eirraplem  11787  p1modz1  11804  dvdsmodexp  11805  moddvds  11809  mulmoddvds  11872  3dvds2dec  11874  zeo3  11876  odd2np1lem  11880  odd2np1  11881  oexpneg  11885  2tp1odd  11892  ltoddhalfle  11901  opoe  11903  opeo  11905  omeo  11906  m1expo  11908  m1exp1  11909  nn0o1gt2  11913  nn0o  11915  divalglemnn  11926  divalglemqt  11927  divalglemeunn  11929  divalglemex  11930  divalglemeuneg  11931  flodddiv4  11942  flodddiv4t2lthalf  11945  gcdaddm  11988  bezoutlemnewy  12000  bezoutlema  12003  bezoutlemb  12004  bezoutlemex  12005  bezoutlemaz  12007  mulgcd  12020  gcddiv  12023  gcdmultiplez  12025  rpmulgcd  12030  rplpwr  12031  uzwodc  12041  lcmgcdlem  12080  lcmgcd  12081  divgcdcoprmex  12105  cncongr2  12107  prmexpb  12154  rpexp  12156  rpexp1i  12157  sqrt2irrlem  12164  oddpwdclemxy  12172  oddpwdclemndvds  12174  sqpweven  12178  2sqpwodd  12179  sqne2sq  12180  qmuldeneqnum  12198  nn0gcdsq  12203  zgcdsq  12204  numdensq  12205  dfphi2  12223  phiprmpw  12225  phiprm  12226  eulerthlema  12233  eulerthlemh  12234  eulerthlemth  12235  fermltl  12237  prmdiv  12238  prmdiveq  12239  prmdivdiv  12240  hashgcdlem  12241  odzval  12244  odzcllem  12245  odzdvds  12248  vfermltl  12254  powm2modprm  12255  reumodprminv  12256  modprm0  12257  nnnn0modprm0  12258  modprmn0modprm0  12259  coprimeprodsq  12260  coprimeprodsq2  12261  pythagtriplem1  12268  pythagtriplem3  12270  pythagtriplem4  12271  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem12  12278  pythagtriplem14  12280  pythagtriplem15  12281  pythagtriplem16  12282  pythagtriplem17  12283  pythagtriplem18  12284  pceu  12298  pczpre  12300  pcdiv  12305  pcqdiv  12310  pcrec  12311  pczndvds  12318  pcneg  12327  pc2dvds  12332  pcprmpw2  12335  pcaddlem  12341  pcadd  12342  fldivp1  12349  pockthlem  12357  pockthi  12359  4sqlem5  12383  4sqlem9  12387  4sqlem10  12388  4sqlem2  12390  4sqlem3  12391  4sqlem4  12393  mul4sqlem  12394  ennnfonelemkh  12416  ennnfonelemhf1o  12417  setscomd  12506  ressressg  12537  qusex  12752  qusin  12753  grprinvlem  12811  grprinvd  12812  grpridd  12813  isnsgrp  12819  sgrpass  12821  sgrp1  12823  mnd12g  12836  mndpropd  12848  mhmlin  12865  grprcan  12917  grpinvid1  12931  isgrpinv  12933  grplcan  12939  grpasscan1  12940  grplmulf1o  12951  grpinvadd  12955  grpinvsub  12959  grpsubsub4  12970  grppnpcan2  12971  grpnpncan  12972  dfgrp3mlem  12975  dfgrp3m  12976  grplactcnv  12979  imasgrp2  12985  mhmlem  12987  mhmid  12988  mhmmnd  12989  mulgnnp1  13001  mulg2  13002  mulgnn0p1  13004  mulgsubcl  13007  mulgneg  13011  mulgaddcomlem  13016  mulgaddcom  13017  mulgz  13021  mulgnn0dir  13023  mulgdirlem  13024  mulgdir  13025  mulgneg2  13027  mulgnnass  13028  mulgnn0ass  13029  mulgass  13030  mulgassr  13031  mulgmodid  13032  mulgsubdir  13033  isnsg3  13077  nmzsubg  13080  ssnmz  13081  0nsg  13084  eqger  13094  eqgid  13096  eqgcpbl  13098  ablsub2inv  13125  abladdsub4  13128  abladdsub  13129  ablpncan2  13130  ablpnpcan  13134  ablnncan  13135  ablnnncan1  13138  mgpress  13152  srgass  13165  srgmulgass  13183  srgpcomp  13184  srgpcompp  13185  srgpcomppsc  13186  ringpropd  13228  ringlz  13233  ring1eq0  13236  ringnegl  13239  ringmneg1  13241  ringsubdir  13245  mulgass2  13246  ring1  13247  opprring  13260  unitgrp  13296  dvrcan1  13320  rdivmuldivd  13324  subrginv  13369  islmod  13392  lmodlema  13393  islmodd  13394  lmod0vs  13422  lmodvs0  13423  lmodvsmmulgdi  13424  lmodvneg1  13431  lmodvsneg  13432  lmodsubvs  13444  lmodsubdi  13445  lmodsubdir  13446  lmodprop2d  13449  rmodislmodlem  13451  rmodislmod  13452  lsssetm  13455  islssmd  13457  lssclg  13462  lssvacl  13463  lss1d  13481  lsspropdg  13529  sraval  13535  resttop  13831  restco  13835  restin  13837  lmfval  13853  cnprcl2k  13867  txrest  13937  txdis1cn  13939  cnmpt2res  13958  psmettri2  13989  psmettri  13991  xmettri2  14022  xmettri  14033  mettri  14034  metrtri  14038  blvalps  14049  blval  14050  xblss2  14066  blhalf  14069  comet  14160  xmetxp  14168  txmetcnp  14179  cnmet  14191  ioo2bl  14204  limcmpted  14293  limcimolemlt  14294  cnplimclemr  14299  limccnp2cntop  14307  reldvg  14309  dvfvalap  14311  dvidlemap  14321  dvconst  14322  dvcnp2cntop  14324  dvaddxxbr  14326  dvmulxxbr  14327  dvcoapbr  14332  dvcjbr  14333  dvexp  14336  dvrecap  14338  dvmptcmulcn  14344  dveflem  14348  sin0pilem1  14363  sinperlem  14390  ptolemy  14406  tangtx  14420  abssinper  14428  reexplog  14453  relogexp  14454  cxprec  14492  rpdivcxp  14493  cxpmul  14494  rpabscxpbnd  14520  rplogbval  14524  rplogbreexp  14532  rprelogbmul  14534  logbrec  14539  logbgcd1irraplemap  14548  binom4  14558  lgslem1  14562  lgslem4  14565  lgsval  14566  lgsfvalg  14567  lgsval2lem  14572  lgsval4lem  14573  lgsvalmod  14581  lgsneg  14586  lgsneg1  14587  lgsmod  14588  lgsdilem  14589  lgsdir2lem4  14593  lgsdir2  14595  lgsdirprm  14596  lgsdir  14597  lgsne0  14600  lgssq  14602  lgssq2  14603  lgsmulsqcoprm  14608  lgsdirnn0  14609  lgsdinn0  14610  lgseisenlem1  14611  lgseisenlem2  14612  m1lgs  14613  2lgsoddprmlem1  14614  2lgsoddprmlem2  14615  2lgsoddprmlem3  14620  2sqlem1  14622  2sqlem2  14623  mul2sq  14624  2sqlem3  14625  2sqlem4  14626  2sqlem8  14631  2sqlem9  14632  2sqlem10  14633  trilpolemeq1  14950  trilpolemlt1  14951  trirec0xor  14955  apdifflemf  14956  apdiff  14958