Theorem oveq1d 5797

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 5789	. 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 1332  (class class class)co 5782

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  fvoveq1d  5804  csbov2g  5820  caovassg  5937  caovdig  5953  caovdirg  5956  caov12d  5960  caov31d  5961  caov411d  5964  grprinvlem  5973  grprinvd  5974  grpridd  5975  caofinvl  6012  omsuc  6376  nnmsucr  6392  nnm1  6428  nnm2  6429  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  addasspig  7162  mulasspig  7164  mulpipq2  7203  distrnqg  7219  ltsonq  7230  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  archnqq  7249  prarloclemarch2  7251  enq0sym  7264  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  nqpnq0nq  7285  nq0m0r  7288  nq0a0  7289  nnanq0  7290  distrnq0  7291  addassnq0  7294  addpinq1  7296  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  prarloclemcalc  7334  addnqprllem  7359  addnqprulem  7360  appdivnq  7395  recexprlem1ssl  7465  recexprlem1ssu  7466  ltmprr  7474  cauappcvgprlemladdru  7488  cauappcvgprlem1  7491  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemexb  7539  caucvgprprlem1  7541  addcmpblnr  7571  mulcmpblnrlemg  7572  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  ltsrprg  7579  1idsr  7600  pn0sr  7603  recexgt0sr  7605  mulgt0sr  7610  srpospr  7615  prsradd  7618  caucvgsrlemfv  7623  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffval  7628  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  caucvgsrlembnd  7633  caucvgsr  7634  map2psrprg  7637  pitonnlem1p1  7678  pitonnlem2  7679  pitonn  7680  recidpirqlemcalc  7689  ax1rid  7709  axrnegex  7711  axcnre  7713  recriota  7722  nntopi  7726  axcaucvglemval  7729  axcaucvglemcau  7730  axcaucvglemres  7731  mul12  7915  mul4  7918  muladd11  7919  readdcan  7926  muladd11r  7942  add12  7944  cnegex  7964  addcan  7966  negeu  7977  pncan2  7993  addsubass  7996  addsub  7997  2addsub  8000  addsubeq4  8001  subid  8005  subid1  8006  npncan  8007  nppcan  8008  nnpcan  8009  nnncan1  8022  npncan3  8024  pnpcan  8025  pnncan  8027  ppncan  8028  addsub4  8029  negsub  8034  subneg  8035  subeqxfrd  8149  mvlraddd  8150  mvlladdd  8151  mvrraddd  8152  subaddeqd  8155  ine0  8180  mulneg1  8181  ltadd2  8205  apreap  8373  cru  8388  recexap  8438  mulcanapd  8446  div23ap  8475  div13ap  8477  divmulassap  8479  divmulasscomap  8480  divcanap4  8483  muldivdirap  8491  divsubdirap  8492  divmuldivap  8496  divdivdivap  8497  divcanap5  8498  divmul13ap  8499  divmuleqap  8501  divdiv32ap  8504  divcanap7  8505  dmdcanap  8506  divdivap1  8507  divdivap2  8508  divadddivap  8511  divsubdivap  8512  conjmulap  8513  divneg2ap  8520  subrecap  8622  mvllmulapd  8625  lt2mul2div  8661  nndivtr  8786  2halves  8973  halfaddsub  8978  avgle1  8984  avgle2  8985  div4p1lem1div2  8997  un0addcl  9034  un0mulcl  9035  peano2z  9114  zneo  9176  nneoor  9177  nneo  9178  zeo  9180  zeo2  9181  deceq1  9210  qreccl  9461  xaddcom  9674  xnegdi  9681  xaddass  9682  xaddass2  9683  xpncan  9684  xleadd1a  9686  xltadd1  9689  xposdif  9695  xadd4d  9698  lincmb01cmp  9816  iccf1o  9817  fzosubel3  10004  qavgle  10067  2tnp1ge0ge0  10105  fldiv4p1lem1div2  10109  ceilqm1lt  10116  flqdiv  10125  modqlt  10137  modqdiffl  10139  modqcyc2  10164  modqaddabs  10166  mulqaddmodid  10168  mulp1mod1  10169  modqmuladd  10170  modqmuladdnn0  10172  qnegmod  10173  addmodid  10176  addmodidr  10177  modqadd2mod  10178  modqm1p1mod0  10179  modqmul12d  10182  modqnegd  10183  modqadd12d  10184  modqsub12d  10185  q2submod  10189  modqmulmodr  10194  modqaddmulmod  10195  modqsubdir  10197  modfzo0difsn  10199  modsumfzodifsn  10200  addmodlteq  10202  frecuzrdgsuc  10218  frecfzennn  10230  iseqovex  10260  seq3-1p  10284  seq3caopr2  10286  seq3caopr  10287  seq3id  10312  seq3homo  10314  seq3z  10315  expp1  10331  exprecap  10365  expaddzaplem  10367  expmulzap  10370  expdivap  10375  sqval  10382  sqsubswap  10384  subsq  10430  subsq2  10431  binom2  10434  binom2sub  10436  mulbinom2  10439  binom3  10440  zesq  10441  bernneq2  10444  sqoddm1div8  10475  nn0opthlem1d  10498  nn0opthd  10500  nn0opth2d  10501  facp1  10508  facdiv  10516  facndiv  10517  faclbnd  10519  faclbnd2  10520  faclbnd3  10521  bcval  10527  bccmpl  10532  bcm1k  10538  bcp1n  10539  bcp1nk  10540  bcval5  10541  bcp1m1  10543  bcpasc  10544  bcn2m1  10547  hashprg  10586  hashdifpr  10598  hashfzo  10600  hashfzp1  10602  hashfz0  10603  hashxp  10604  zfz1isolemsplit  10613  zfz1isolem1  10615  seq3coll  10617  reval  10653  crre  10661  remim  10664  remul2  10677  immul2  10684  imval2  10698  cjdivap  10713  caucvgre  10785  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemp1rp  10810  resqrexlemfp1  10813  resqrexlemover  10814  resqrexlemcalc1  10818  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  resqrexlemsqa  10828  resqrexlemex  10829  resqrex  10830  sqrtdiv  10846  absvalsq  10857  absreimsq  10871  absdivap  10874  cau3lem  10918  maxabslemlub  11011  maxabslemval  11012  max0addsup  11023  minabs  11039  bdtrilem  11042  bdtri  11043  xrmaxaddlem  11061  xrmaxadd  11062  xrbdtri  11077  clim  11082  clim2  11084  climshftlemg  11103  climshft2  11107  climcn1  11109  climcn2  11110  subcn2  11112  reccn2ap  11114  climmulc2  11132  climsubc2  11134  clim2ser  11138  iser3shft  11147  climcau  11148  serf0  11153  fzosump1  11218  fsum1p  11219  fsump1  11221  sumsplitdc  11233  fsump1i  11234  mptfzshft  11243  fisum0diag2  11248  fsumconst  11255  fsumdifsnconst  11256  modfsummodlemstep  11258  modfsummod  11259  telfsumo  11267  fsumparts  11271  fsumrelem  11272  hash2iun1dif1  11281  binomlem  11284  binom  11285  binom1p  11286  binom1dif  11288  bcxmas  11290  isumsplit  11292  isum1p  11293  arisum  11299  arisum2  11300  trireciplem  11301  geoserap  11308  geolim  11312  geolim2  11313  georeclim  11314  geo2sum  11315  geoisum1  11320  cvgratnnlemseq  11327  cvgratnnlemsumlt  11329  cvgratnnlemfm  11330  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  efcllemp  11401  ef0lem  11403  efval  11404  esum  11405  ege2le3  11414  efaddlem  11417  efsep  11434  effsumlt  11435  eft0val  11436  efgt1p2  11438  efgt1p  11439  sinval  11445  cosval  11446  resinval  11458  recosval  11459  efi4p  11460  resin4p  11461  recos4p  11462  sinneg  11469  cosneg  11470  efival  11475  sinadd  11479  cosadd  11480  tanaddap  11482  sinmul  11487  cosmul  11488  cos2t  11493  cos2tsin  11494  ef01bndlem  11499  absefib  11513  demoivre  11515  demoivreALT  11516  eirraplem  11519  moddvds  11538  mulmoddvds  11597  3dvds2dec  11599  zeo3  11601  odd2np1lem  11605  odd2np1  11606  oexpneg  11610  2tp1odd  11617  ltoddhalfle  11626  opoe  11628  opeo  11630  omeo  11631  m1expo  11633  m1exp1  11634  nn0o1gt2  11638  nn0o  11640  divalglemnn  11651  divalglemqt  11652  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  flodddiv4  11667  flodddiv4t2lthalf  11670  gcdaddm  11708  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  bezoutlemex  11725  bezoutlemaz  11727  mulgcd  11740  gcddiv  11743  gcdmultiplez  11745  rpmulgcd  11750  rplpwr  11751  lcmgcdlem  11794  lcmgcd  11795  divgcdcoprmex  11819  cncongr2  11821  prmexpb  11865  rpexp  11867  rpexp1i  11868  sqrt2irrlem  11875  oddpwdclemxy  11883  oddpwdclemndvds  11885  sqpweven  11889  2sqpwodd  11890  sqne2sq  11891  qmuldeneqnum  11909  nn0gcdsq  11914  zgcdsq  11915  numdensq  11916  dfphi2  11932  phiprmpw  11934  phiprm  11935  hashgcdlem  11939  ennnfonelemkh  11961  ennnfonelemhf1o  11962  resttop  12378  restco  12382  restin  12384  lmfval  12400  cnprcl2k  12414  txrest  12484  txdis1cn  12486  cnmpt2res  12505  psmettri2  12536  psmettri  12538  xmettri2  12569  xmettri  12580  mettri  12581  metrtri  12585  blvalps  12596  blval  12597  xblss2  12613  blhalf  12616  comet  12707  xmetxp  12715  txmetcnp  12726  cnmet  12738  ioo2bl  12751  limcmpted  12840  limcimolemlt  12841  cnplimclemr  12846  limccnp2cntop  12854  reldvg  12856  dvfvalap  12858  dvidlemap  12868  dvconst  12869  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvexp  12883  dvrecap  12885  dvmptcmulcn  12891  dveflem  12895  sin0pilem1  12910  sinperlem  12937  ptolemy  12953  tangtx  12967  abssinper  12975  reexplog  13000  relogexp  13001  cxprec  13039  rpdivcxp  13040  cxpmul  13041  rpabscxpbnd  13067  rplogbval  13070  rplogbreexp  13078  rprelogbmul  13080  logbrec  13085  logbgcd1irraplemap  13094  trilpolemeq1  13408  trilpolemlt1  13409  trirec0xor  13413  apdifflemf  13414  apdiff  13416