Theorem oveq2d 5972

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveq2d	|- ( ph -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq2 5964	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1373  (class class class)co 5956

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-iota 5240  df-fv 5287  df-ov 5959

This theorem is referenced by:  csbov1g  5997  caovassg  6117  caovdig  6133  caovdirg  6136  caov32d  6139  caov4d  6143  caov42d  6145  nnaass  6583  nndi  6584  nnmass  6585  nnmsucr  6586  ecovass  6743  ecoviass  6744  ecovdi  6745  ecovidi  6746  addasspig  7458  mulasspig  7460  distrpig  7461  dfplpq2  7482  mulpipq2  7499  addassnqg  7510  prarloclemarch  7546  prarloclemarch2  7547  ltrnqg  7548  enq0sym  7560  addnq0mo  7575  mulnq0mo  7576  addnnnq0  7577  nq0a0  7585  distrnq0  7587  addassnq0  7590  prarloclemlo  7622  prarloclem3  7625  prarloclem5  7628  prarloclemcalc  7630  addnqprl  7657  addnqpru  7658  prmuloclemcalc  7693  mulnqprl  7696  mulnqpru  7697  distrlem4prl  7712  distrlem4pru  7713  1idprl  7718  1idpru  7719  ltexprlemloc  7735  addcanprleml  7742  addcanprlemu  7743  recexprlem1ssu  7762  ltmprr  7770  caucvgprlemcanl  7772  cauappcvgprlemladdru  7784  cauappcvgprlemladdrl  7785  cauappcvgprlem1  7787  cauappcvgprlemlim  7789  caucvgprlemnkj  7794  caucvgprlemnbj  7795  caucvgprlemdisj  7802  caucvgprlemloc  7803  caucvgprlemcl  7804  caucvgprlemladdrl  7806  caucvgprlem1  7807  caucvgpr  7810  caucvgprprlemell  7813  caucvgprprlemcbv  7815  caucvgprprlemval  7816  caucvgprprlemnkeqj  7818  caucvgprprlemopl  7825  caucvgprprlemlol  7826  caucvgprprlemloc  7831  caucvgprprlemclphr  7833  caucvgprprlemexb  7835  caucvgprprlemaddq  7836  caucvgprprlem1  7837  addcmpblnr  7867  mulcmpblnrlemg  7868  addsrmo  7871  mulsrmo  7872  addsrpr  7873  mulsrpr  7874  ltsrprg  7875  recexgt0sr  7901  mulgt0sr  7906  caucvgsrlemgt1  7923  caucvgsrlemoffval  7924  caucvgsr  7930  suplocsrlemb  7934  suplocsrlempr  7935  suplocsrlem  7936  suplocsr  7937  mulcnsr  7963  pitoregt0  7977  recidpirqlemcalc  7985  axmulcom  7999  axmulass  8001  axdistr  8002  ax0id  8006  axcnre  8009  recriota  8018  axcaucvglemcau  8026  axcaucvglemres  8027  mulrid  8084  adddirp1d  8114  mul32  8217  mul31  8218  add32  8246  add4  8248  add42  8249  cnegex  8265  addcan2  8268  addsubass  8297  subsub2  8315  nppcan2  8318  sub32  8321  nnncan  8322  sub4  8332  muladd  8471  subdi  8472  mul2neg  8485  submul2  8486  mulsub  8488  muls1d  8505  mulsubfacd  8506  add20  8562  recexre  8666  rereim  8674  apreap  8675  ltmul1  8680  cru  8690  apreim  8691  mulreim  8692  apadd1  8696  apneg  8699  mulap0  8742  divrecap  8776  divassap  8778  divmulasscomap  8784  divsubdirap  8796  divdivdivap  8801  divmul24ap  8804  divmuleqap  8805  divcanap6  8807  divdivap1  8811  divdivap2  8812  divsubdivap  8816  conjmulap  8817  div2negap  8823  apmul1  8876  cju  9049  nnmulcl  9072  add1p1  9302  sub1m1  9303  cnm2m1cnm3  9304  xp1d2m1eqxm1d2  9305  div4p1lem1div2  9306  un0addcl  9343  un0mulcl  9344  zaddcllemneg  9426  qapne  9775  cnref1o  9787  rexsub  9990  xnegid  9996  xaddcom  9998  xnegdi  10005  xaddass  10006  xaddass2  10007  xpncan  10008  xnpcan  10009  xleadd1a  10010  xsubge0  10018  xposdif  10019  xlesubadd  10020  xadd4d  10022  lincmb01cmp  10140  iccf1o  10141  ige3m2fz  10186  fztp  10215  fzsuc2  10216  fseq1m1p1  10232  fzm1  10237  ige2m1fz1  10246  nn0split  10273  nnsplit  10274  fzo0addelr  10335  elfzoext  10338  fzval3  10350  zpnn0elfzo1  10354  fzosplitsnm1  10355  fzosplitprm1  10380  fzoshftral  10384  rebtwn2zlemstep  10412  flhalf  10462  fldiv4lem1div2uz2  10466  modqval  10486  modqvalr  10487  modqdiffl  10497  modqfrac  10499  flqmod  10500  intqfrac  10501  zmod10  10502  modqmulnn  10504  modqvalp1  10505  modqid  10511  modqcyc  10521  modqcyc2  10522  modqmul1  10539  q2submod  10547  modqdi  10554  modqsubdir  10555  modqeqmodmin  10556  modsumfzodifsn  10558  addmodlteq  10560  frecuzrdgsuctlem  10585  uzsinds  10606  seqeq3  10614  iseqvalcbv  10621  seq3val  10622  seqvalcd  10623  seqf  10626  seq3p1  10627  seqovcd  10629  seqp1cd  10632  seq3m1  10635  seq3fveq2  10637  seqfveq2g  10639  seq3shft2  10643  seqshft2g  10644  monoord2  10648  ser3mono  10649  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seqcaopr3g  10654  seq3caopr2  10655  seqcaopr2g  10656  seq3caopr  10657  seqcaoprg  10658  seqf1oglem2a  10680  seqf1oglem2  10682  seq3id2  10688  seq3homo  10689  seq3z  10690  seqhomog  10692  exp3vallem  10702  exp3val  10703  expp1  10708  expnegap0  10709  expineg2  10710  expn1ap0  10711  expm1t  10729  1exp  10730  expnegzap  10735  mulexpzap  10741  expadd  10743  expaddzaplem  10744  expaddzap  10745  expmul  10746  expmulzap  10747  m1expeven  10748  expsubap  10749  expp1zap  10750  expm1ap  10751  expdivap  10752  iexpcyc  10806  subsq2  10809  binom2  10813  binom21  10814  binom2sub  10815  binom2sub1  10816  mulbinom2  10818  binom3  10819  zesq  10820  bernneq  10822  sqoddm1div8  10855  mulsubdivbinom2ap  10873  nn0opthlem1d  10882  nn0opthd  10884  facp1  10892  facnn2  10896  faclbnd  10903  faclbnd6  10906  bcval  10911  bccmpl  10916  bcn0  10917  bcnn  10919  bcnp1n  10921  bcm1k  10922  bcp1n  10923  bcp1nk  10924  bcval5  10925  bcp1m1  10927  bcpasc  10928  bcn2m1  10931  bcn2p1  10932  omgadd  10964  hashunlem  10966  hashunsng  10969  hashdifsn  10981  hashxp  10988  zfz1isolemsplit  11000  zfz1isolem1  11002  zfz1iso  11003  seq3coll  11004  wrdf  11017  ccatfvalfi  11066  elfzelfzccat  11074  ccatlid  11080  ccatrid  11081  ccatass  11082  ccatws1leng  11106  ccats1val2  11110  swrdval  11119  swrd00g  11120  swrdf  11126  swrdfv2  11134  swrdwrdsymbg  11135  swrdspsleq  11138  swrds1  11139  swrdlsw  11140  ccatswrd  11141  swrdccat2  11142  pfxmpt  11151  pfxfv  11155  pfxeq  11167  pfxsuff1eqwrdeq  11170  ccatpfx  11172  pfxccat1  11173  swrdswrd  11176  pfxswrd  11177  swrdpfx  11178  pfxpfx  11179  pfxlswccat  11184  ccats1pfxeq  11185  ccats1pfxeqrex  11186  ccatopth2  11188  cats1un  11192  wrdind  11193  wrd2ind  11194  shftcan1  11215  shftcan2  11216  cjval  11226  cjth  11227  crre  11238  replim  11240  remim  11241  reim0b  11243  rereb  11244  mulreap  11245  cjreb  11247  recj  11248  reneg  11249  readd  11250  resub  11251  remullem  11252  imcj  11256  imneg  11257  imadd  11258  imsub  11259  cjcj  11264  cjadd  11265  ipcnval  11267  cjmulrcl  11268  cjneg  11271  addcj  11272  cjsub  11273  cnrecnv  11291  caucvgrelemcau  11361  cvg1nlemcau  11365  cvg1nlemres  11366  recvguniqlem  11375  resqrexlemover  11391  resqrexlemlo  11394  resqrexlemcalc1  11395  resqrexlemcalc3  11397  resqrexlemnm  11399  resqrexlemcvg  11400  absneg  11431  abscj  11433  sqabsadd  11436  sqabssub  11437  absmul  11450  absid  11452  absre  11458  absresq  11459  absexpzap  11461  recvalap  11478  abstri  11485  abs2dif2  11488  recan  11490  cau3lem  11495  amgm2  11499  bdtrilem  11620  xrmaxadd  11642  xrbdtri  11657  climaddc1  11710  climsubc1  11713  climcvg1nlem  11730  serf0  11733  summodclem3  11761  summodclem2a  11762  summodc  11764  fsumsplitsn  11791  fsumm1  11797  fsumsplitsnun  11800  fsump1  11801  isummulc2  11807  fsumrev  11824  fisum0diag2  11828  fsummulc2  11829  fsumsub  11833  fsumabs  11846  telfsumo  11847  fsumparts  11851  fsumrelem  11852  fsumiun  11858  binomlem  11864  binom  11865  binom1p  11866  binom11  11867  binom1dif  11868  bcxmas  11870  isumsplit  11872  isum1p  11873  divcnv  11878  arisum2  11880  trireciplem  11881  trirecip  11882  geolim  11892  georeclim  11894  geo2sum  11895  geo2lim  11897  geoisum1c  11901  0.999...  11902  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  cvgratz  11913  mertenslem2  11917  mertensabs  11918  clim2prod  11920  prodfrecap  11927  prodfdivap  11928  prodmodclem3  11956  prodmodclem2a  11957  fprodm1  11979  fprodp1  11981  fprodunsn  11985  fprodfac  11996  fprodeq0  11998  fprodconst  12001  fprodrec  12010  fproddivap  12011  fprodsplitsn  12014  ege2le3  12052  efaddlem  12055  efsub  12062  efexp  12063  eftlub  12071  efsep  12072  effsumlt  12073  ef4p  12075  tanval3ap  12095  resinval  12096  recosval  12097  efi4p  12098  efival  12113  efmival  12114  efeul  12115  sinadd  12117  cosadd  12118  tanaddap  12120  sinsub  12121  cossub  12122  sincossq  12129  sin2t  12130  cos2t  12131  cos2tsin  12132  ef01bndlem  12137  sin01bnd  12138  cos01bnd  12139  cos12dec  12149  absef  12151  absefib  12152  efieq1re  12153  demoivreALT  12155  eirraplem  12158  dvdsexp  12242  oexpneg  12258  opeo  12278  omeo  12279  m1exp1  12282  flodddiv4  12317  flodddiv4t2lthalf  12320  bitsval  12324  bitsp1  12332  bitsinv1lem  12342  bitsinv1  12343  divgcdnnr  12367  gcdaddm  12375  gcdadd  12376  gcdid  12377  modgcd  12382  gcdmultipled  12384  dvdsgcdidd  12385  bezoutlemnewy  12387  bezoutlema  12390  bezoutlemb  12391  bezoutlemex  12392  bezoutlembz  12395  absmulgcd  12408  gcdmultiple  12411  gcdmultiplez  12412  rpmulgcd  12417  rplpwr  12418  eucalginv  12448  eucalg  12451  lcmneg  12466  lcmgcdlem  12469  lcmgcd  12470  lcmid  12472  lcm1  12473  mulgcddvds  12486  qredeq  12488  divgcdcoprmex  12494  prmind2  12512  rpexp1i  12546  pw2dvdslemn  12557  pw2dvdseulemle  12559  pw2dvdseu  12560  oddpwdclemxy  12561  oddpwdclemdvds  12562  oddpwdclemndvds  12563  oddpwdclemdc  12565  2sqpwodd  12568  nn0gcdsq  12592  phiprmpw  12614  eulerthlemrprm  12621  eulerthlema  12622  eulerthlemh  12623  eulerthlemth  12624  fermltl  12626  prmdiv  12627  hashgcdlem  12630  odzdvds  12638  vfermltl  12644  modprm0  12647  nnnn0modprm0  12648  modprmn0modprm0  12649  coprimeprodsq  12650  pythagtriplem1  12658  pythagtriplem4  12661  pythagtriplem12  12668  pythagtriplem14  12670  pythagtriplem16  12672  pythagtriplem18  12674  pythagtrip  12676  pcpremul  12686  pceu  12688  pczpre  12690  pcdiv  12695  pcqmul  12696  pcqdiv  12700  pcexp  12702  pcxqcl  12705  pczdvds  12707  pczndvds  12709  pczndvds2  12711  pcid  12717  pcneg  12718  pcdvdstr  12720  pcgcd1  12721  pcgcd  12722  pc2dvds  12723  pcaddlem  12732  pcadd  12733  pcadd2  12734  pcmpt  12736  pcmpt2  12737  fldivp1  12741  pcfac  12743  pcbc  12744  expnprm  12746  prmpwdvds  12748  pockthlem  12749  pockthi  12751  4sqlem7  12777  4sqlem9  12779  4sqlem10  12780  4sqlem2  12782  4sqlem3  12783  4sqlem4  12785  mul4sqlem  12786  4sqlem11  12794  4sqlem16  12799  4sqlem17  12800  4sqlem19  12802  setscomd  12943  ressvalsets  12966  strressid  12973  ressval3d  12974  ressinbasd  12976  ressressg  12977  ressabsg  12978  grpinvalem  13287  grpinva  13288  grprida  13289  isnsgrp  13308  sgrpass  13310  sgrp1  13313  sgrppropd  13315  prdssgrpd  13317  mnd32g  13329  mnd4g  13331  mndpropd  13342  prdsidlem  13349  prdsmndd  13350  imasmnd2  13354  mhmex  13364  mhmlin  13369  gsumwmhm  13400  grprcan  13439  grpsubval  13448  grpinvid2  13455  grpasscan2  13466  grpsubinv  13475  grpinvadd  13480  grpsubid1  13487  grpsubadd0sub  13489  grpsubadd  13490  grpsubsub  13491  grpaddsubass  13492  grppncan  13493  grpnnncan2  13499  grpsubpropd2  13507  imasgrp2  13516  mhmlem  13520  mhmid  13521  mhmmnd  13522  ghmgrp  13524  mulgnn0gsum  13534  mulgnnp1  13536  mulgaddcomlem  13551  mulgaddcom  13552  mulginvinv  13554  mulgnn0dir  13558  mulgdirlem  13559  mulgp1  13561  mulgneg2  13562  mulgnn0ass  13564  mulgass  13565  mulgmodid  13567  mulgsubdir  13568  nmzsubg  13616  0nsg  13620  eqger  13630  qussub  13643  ghmlin  13654  ghmsub  13657  conjghm  13682  ablsub4  13719  abladdsub4  13720  ablsubsub4  13725  ablsub32  13728  ablnnncan  13729  gsumfzmptfidmadd2  13746  gsumfzconst  13747  gsumfzmhm2  13750  gsumfzsnfd  13751  mgpress  13763  rngass  13771  rngdi  13772  rngdir  13773  rngrz  13778  rngmneg2  13780  rngsubdi  13783  rngsubdir  13784  rngpropd  13787  imasrng  13788  srgass  13803  srgpcomp  13822  srgpcompp  13823  srgpcomppsc  13824  srg1expzeq1  13827  ringpropd  13870  ringrz  13876  ringnegr  13884  ringmneg2  13886  ringsubdi  13888  ringsubdir  13889  ring1  13891  imasring  13896  opprrng  13909  opprring  13911  mulgass3  13917  dvdsrd  13926  unitgrp  13948  invrfvald  13954  dvr1  13970  dvrass  13971  dvrcan1  13972  dvrcan3  13973  rdivmuldivd  13976  subrginv  14069  subrgdv  14070  resrhm2b  14081  islmod  14123  lmodlema  14124  islmodd  14125  lmodvs0  14154  lmodvneg1  14162  lmodvsubval2  14174  lmodsubvs  14175  lmodsubdi  14176  lmodsubdir  14177  lmodprop2d  14180  rmodislmodlem  14182  rmodislmod  14183  lsssn0  14202  sraval  14269  cnfldsub  14407  gsumfzfsumlem0  14418  gsumfzfsumlemm  14419  mulgrhm  14441  mulgrhm2  14442  znval  14468  znval2  14470  znunit  14491  psrval  14498  mplvalcoe  14522  mplval2g  14527  restabs  14717  cnprcl2k  14748  cnrest2r  14779  ispsmet  14865  psmettri2  14870  psmetsym  14871  ismet  14886  isxmet  14887  xmettri2  14903  xmetsym  14910  xmettri3  14916  mettri3  14917  xblss2ps  14946  xblss2  14947  comet  15041  xmetxp  15049  xmetxpbl  15050  txmetcnp  15060  fsumcncntop  15109  cncfi  15120  divcncfap  15156  limccl  15201  ellimc3apf  15202  limccnpcntop  15217  limccnp2lem  15218  reldvg  15221  dvfvalap  15223  eldvap  15224  dvcj  15251  dvfre  15252  dvexp  15253  dvexp2  15254  dvrecap  15255  dvmptaddx  15261  dvmptmulx  15262  dvmptnegcn  15264  dvmptsubcn  15265  dvmptcjx  15266  dvmptfsum  15267  dveflem  15268  dvef  15269  plyconst  15287  plyaddlem1  15289  plymullem1  15290  plyadd  15293  plymul  15294  plycoeid3  15299  plycolemc  15300  plyco  15301  plycjlemc  15302  plycj  15303  plyrecj  15305  dvply1  15307  dvply2g  15308  sin0pilem1  15323  sin0pilem2  15324  efper  15349  sinperlem  15350  efimpi  15361  ptolemy  15366  tangtx  15380  abssinper  15388  cosq34lt1  15392  rpcxpef  15436  rpcxpp1  15448  rpcxpneg  15449  rpcxpsub  15450  rpmulcxp  15451  rpdivcxp  15453  cxpmul  15454  rpcxpmul2  15455  rpcxproot  15456  cxpcom  15480  rpabscxpbnd  15482  rplogbval  15487  rplogbreexp  15495  rplogbzexp  15496  rprelogbmulexp  15498  rprelogbdiv  15499  relogbexpap  15500  rplogbcxp  15505  rpcxplogb  15506  logbgcd1irr  15509  logbgcd1irraplemap  15511  binom4  15521  wilthlem1  15522  sgmval  15525  sgmppw  15534  1sgmprm  15536  mersenne  15539  perfectlem1  15541  perfectlem2  15542  perfect  15543  lgslem1  15547  lgsval  15551  lgsfvalg  15552  lgsval2lem  15557  lgsval4  15567  lgsneg  15571  lgsneg1  15572  lgsmod  15573  lgsdir2  15580  lgsdirprm  15581  lgsdilem2  15583  lgsdi  15584  lgsne0  15585  lgssq2  15588  lgsdirnn0  15594  lgsdinn0  15595  gausslemma2dlem1a  15605  gausslemma2dlem1f1o  15607  gausslemma2dlem2  15609  gausslemma2dlem3  15610  gausslemma2dlem4  15611  gausslemma2dlem5  15613  gausslemma2dlem6  15614  gausslemma2d  15616  lgseisenlem1  15617  lgseisenlem2  15618  lgseisenlem3  15619  lgseisenlem4  15620  lgsquadlem1  15624  lgsquadlem2  15625  lgsquadlem3  15626  lgsquad2lem1  15628  lgsquad2lem2  15629  lgsquad2  15630  lgsquad3  15631  m1lgs  15632  2lgslem3c  15642  2lgslem3d  15643  2lgslem3d1  15647  2sqlem2  15662  2sqlem3  15664  2sqlem4  15665  2sqlem8  15670  2sqlem9  15671  2sqlem10  15672  qdencn  16101  trilpolemclim  16110  trilpolemcl  16111  trilpolemisumle  16112  trilpolemeq1  16114  trilpolemlt1  16115  trilpo  16117  apdifflemf  16120  apdiff  16122  iswomni0  16125  redcwlpolemeq1  16128  redcwlpo  16129  nconstwlpolem0  16137  nconstwlpolemgt0  16138  nconstwlpo  16140  neapmkv  16142