Theorem oveq2d 5962

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 5954	. 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 5946

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  csbov1g  5987  caovassg  6107  caovdig  6123  caovdirg  6126  caov32d  6129  caov4d  6133  caov42d  6135  nnaass  6573  nndi  6574  nnmass  6575  nnmsucr  6576  ecovass  6733  ecoviass  6734  ecovdi  6735  ecovidi  6736  addasspig  7445  mulasspig  7447  distrpig  7448  dfplpq2  7469  mulpipq2  7486  addassnqg  7497  prarloclemarch  7533  prarloclemarch2  7534  ltrnqg  7535  enq0sym  7547  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  nq0a0  7572  distrnq0  7574  addassnq0  7577  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  prarloclemcalc  7617  addnqprl  7644  addnqpru  7645  prmuloclemcalc  7680  mulnqprl  7683  mulnqpru  7684  distrlem4prl  7699  distrlem4pru  7700  1idprl  7705  1idpru  7706  ltexprlemloc  7722  addcanprleml  7729  addcanprlemu  7730  recexprlem1ssu  7749  ltmprr  7757  caucvgprlemcanl  7759  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnkeqj  7805  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexb  7822  caucvgprprlemaddq  7823  caucvgprprlem1  7824  addcmpblnr  7854  mulcmpblnrlemg  7855  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  ltsrprg  7862  recexgt0sr  7888  mulgt0sr  7893  caucvgsrlemgt1  7910  caucvgsrlemoffval  7911  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  suplocsr  7924  mulcnsr  7950  pitoregt0  7964  recidpirqlemcalc  7972  axmulcom  7986  axmulass  7988  axdistr  7989  ax0id  7993  axcnre  7996  recriota  8005  axcaucvglemcau  8013  axcaucvglemres  8014  mulrid  8071  adddirp1d  8101  mul32  8204  mul31  8205  add32  8233  add4  8235  add42  8236  cnegex  8252  addcan2  8255  addsubass  8284  subsub2  8302  nppcan2  8305  sub32  8308  nnncan  8309  sub4  8319  muladd  8458  subdi  8459  mul2neg  8472  submul2  8473  mulsub  8475  muls1d  8492  mulsubfacd  8493  add20  8549  recexre  8653  rereim  8661  apreap  8662  ltmul1  8667  cru  8677  apreim  8678  mulreim  8679  apadd1  8683  apneg  8686  mulap0  8729  divrecap  8763  divassap  8765  divmulasscomap  8771  divsubdirap  8783  divdivdivap  8788  divmul24ap  8791  divmuleqap  8792  divcanap6  8794  divdivap1  8798  divdivap2  8799  divsubdivap  8803  conjmulap  8804  div2negap  8810  apmul1  8863  cju  9036  nnmulcl  9059  add1p1  9289  sub1m1  9290  cnm2m1cnm3  9291  xp1d2m1eqxm1d2  9292  div4p1lem1div2  9293  un0addcl  9330  un0mulcl  9331  zaddcllemneg  9413  qapne  9762  cnref1o  9774  rexsub  9977  xnegid  9983  xaddcom  9985  xnegdi  9992  xaddass  9993  xaddass2  9994  xpncan  9995  xnpcan  9996  xleadd1a  9997  xsubge0  10005  xposdif  10006  xlesubadd  10007  xadd4d  10009  lincmb01cmp  10127  iccf1o  10128  ige3m2fz  10173  fztp  10202  fzsuc2  10203  fseq1m1p1  10219  fzm1  10224  ige2m1fz1  10233  nn0split  10260  nnsplit  10261  fzo0addelr  10320  elfzoext  10323  fzval3  10335  zpnn0elfzo1  10339  fzosplitsnm1  10340  fzosplitprm1  10365  fzoshftral  10369  rebtwn2zlemstep  10397  flhalf  10447  fldiv4lem1div2uz2  10451  modqval  10471  modqvalr  10472  modqdiffl  10482  modqfrac  10484  flqmod  10485  intqfrac  10486  zmod10  10487  modqmulnn  10489  modqvalp1  10490  modqid  10496  modqcyc  10506  modqcyc2  10507  modqmul1  10524  q2submod  10532  modqdi  10539  modqsubdir  10540  modqeqmodmin  10541  modsumfzodifsn  10543  addmodlteq  10545  frecuzrdgsuctlem  10570  uzsinds  10591  seqeq3  10599  iseqvalcbv  10606  seq3val  10607  seqvalcd  10608  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3m1  10620  seq3fveq2  10622  seqfveq2g  10624  seq3shft2  10628  seqshft2g  10629  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr2  10640  seqcaopr2g  10641  seq3caopr  10642  seqcaoprg  10643  seqf1oglem2a  10665  seqf1oglem2  10667  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  exp3vallem  10687  exp3val  10688  expp1  10693  expnegap0  10694  expineg2  10695  expn1ap0  10696  expm1t  10714  1exp  10715  expnegzap  10720  mulexpzap  10726  expadd  10728  expaddzaplem  10729  expaddzap  10730  expmul  10731  expmulzap  10732  m1expeven  10733  expsubap  10734  expp1zap  10735  expm1ap  10736  expdivap  10737  iexpcyc  10791  subsq2  10794  binom2  10798  binom21  10799  binom2sub  10800  binom2sub1  10801  mulbinom2  10803  binom3  10804  zesq  10805  bernneq  10807  sqoddm1div8  10840  mulsubdivbinom2ap  10858  nn0opthlem1d  10867  nn0opthd  10869  facp1  10877  facnn2  10881  faclbnd  10888  faclbnd6  10891  bcval  10896  bccmpl  10901  bcn0  10902  bcnn  10904  bcnp1n  10906  bcm1k  10907  bcp1n  10908  bcp1nk  10909  bcval5  10910  bcp1m1  10912  bcpasc  10913  bcn2m1  10916  bcn2p1  10917  omgadd  10949  hashunlem  10951  hashunsng  10954  hashdifsn  10966  hashxp  10973  zfz1isolemsplit  10985  zfz1isolem1  10987  zfz1iso  10988  seq3coll  10989  wrdf  11002  ccatfvalfi  11051  elfzelfzccat  11059  ccatlid  11065  ccatrid  11066  ccatass  11067  ccatws1leng  11091  ccats1val2  11095  swrdval  11104  swrd00g  11105  swrdf  11111  swrdfv2  11119  swrdwrdsymbg  11120  swrdspsleq  11123  swrds1  11124  swrdlsw  11125  ccatswrd  11126  swrdccat2  11127  pfxmpt  11134  pfxfv  11138  pfxeq  11150  pfxsuff1eqwrdeq  11153  ccatpfx  11155  pfxccat1  11156  shftcan1  11178  shftcan2  11179  cjval  11189  cjth  11190  crre  11201  replim  11203  remim  11204  reim0b  11206  rereb  11207  mulreap  11208  cjreb  11210  recj  11211  reneg  11212  readd  11213  resub  11214  remullem  11215  imcj  11219  imneg  11220  imadd  11221  imsub  11222  cjcj  11227  cjadd  11228  ipcnval  11230  cjmulrcl  11231  cjneg  11234  addcj  11235  cjsub  11236  cnrecnv  11254  caucvgrelemcau  11324  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniqlem  11338  resqrexlemover  11354  resqrexlemlo  11357  resqrexlemcalc1  11358  resqrexlemcalc3  11360  resqrexlemnm  11362  resqrexlemcvg  11363  absneg  11394  abscj  11396  sqabsadd  11399  sqabssub  11400  absmul  11413  absid  11415  absre  11421  absresq  11422  absexpzap  11424  recvalap  11441  abstri  11448  abs2dif2  11451  recan  11453  cau3lem  11458  amgm2  11462  bdtrilem  11583  xrmaxadd  11605  xrbdtri  11620  climaddc1  11673  climsubc1  11676  climcvg1nlem  11693  serf0  11696  summodclem3  11724  summodclem2a  11725  summodc  11727  fsumsplitsn  11754  fsumm1  11760  fsumsplitsnun  11763  fsump1  11764  isummulc2  11770  fsumrev  11787  fisum0diag2  11791  fsummulc2  11792  fsumsub  11796  fsumabs  11809  telfsumo  11810  fsumparts  11814  fsumrelem  11815  fsumiun  11821  binomlem  11827  binom  11828  binom1p  11829  binom11  11830  binom1dif  11831  bcxmas  11833  isumsplit  11835  isum1p  11836  divcnv  11841  arisum2  11843  trireciplem  11844  trirecip  11845  geolim  11855  georeclim  11857  geo2sum  11858  geo2lim  11860  geoisum1c  11864  0.999...  11865  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratz  11876  mertenslem2  11880  mertensabs  11881  clim2prod  11883  prodfrecap  11890  prodfdivap  11891  prodmodclem3  11919  prodmodclem2a  11920  fprodm1  11942  fprodp1  11944  fprodunsn  11948  fprodfac  11959  fprodeq0  11961  fprodconst  11964  fprodrec  11973  fproddivap  11974  fprodsplitsn  11977  ege2le3  12015  efaddlem  12018  efsub  12025  efexp  12026  eftlub  12034  efsep  12035  effsumlt  12036  ef4p  12038  tanval3ap  12058  resinval  12059  recosval  12060  efi4p  12061  efival  12076  efmival  12077  efeul  12078  sinadd  12080  cosadd  12081  tanaddap  12083  sinsub  12084  cossub  12085  sincossq  12092  sin2t  12093  cos2t  12094  cos2tsin  12095  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  cos12dec  12112  absef  12114  absefib  12115  efieq1re  12116  demoivreALT  12118  eirraplem  12121  dvdsexp  12205  oexpneg  12221  opeo  12241  omeo  12242  m1exp1  12245  flodddiv4  12280  flodddiv4t2lthalf  12283  bitsval  12287  bitsp1  12295  bitsinv1lem  12305  bitsinv1  12306  divgcdnnr  12330  gcdaddm  12338  gcdadd  12339  gcdid  12340  modgcd  12345  gcdmultipled  12347  dvdsgcdidd  12348  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  bezoutlemex  12355  bezoutlembz  12358  absmulgcd  12371  gcdmultiple  12374  gcdmultiplez  12375  rpmulgcd  12380  rplpwr  12381  eucalginv  12411  eucalg  12414  lcmneg  12429  lcmgcdlem  12432  lcmgcd  12433  lcmid  12435  lcm1  12436  mulgcddvds  12449  qredeq  12451  divgcdcoprmex  12457  prmind2  12475  rpexp1i  12509  pw2dvdslemn  12520  pw2dvdseulemle  12522  pw2dvdseu  12523  oddpwdclemxy  12524  oddpwdclemdvds  12525  oddpwdclemndvds  12526  oddpwdclemdc  12528  2sqpwodd  12531  nn0gcdsq  12555  phiprmpw  12577  eulerthlemrprm  12584  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  fermltl  12589  prmdiv  12590  hashgcdlem  12593  odzdvds  12601  vfermltl  12607  modprm0  12610  nnnn0modprm0  12611  modprmn0modprm0  12612  coprimeprodsq  12613  pythagtriplem1  12621  pythagtriplem4  12624  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pythagtriplem18  12637  pythagtrip  12639  pcpremul  12649  pceu  12651  pczpre  12653  pcdiv  12658  pcqmul  12659  pcqdiv  12663  pcexp  12665  pcxqcl  12668  pczdvds  12670  pczndvds  12672  pczndvds2  12674  pcid  12680  pcneg  12681  pcdvdstr  12683  pcgcd1  12684  pcgcd  12685  pc2dvds  12686  pcaddlem  12695  pcadd  12696  pcadd2  12697  pcmpt  12699  pcmpt2  12700  fldivp1  12704  pcfac  12706  pcbc  12707  expnprm  12709  prmpwdvds  12711  pockthlem  12712  pockthi  12714  4sqlem7  12740  4sqlem9  12742  4sqlem10  12743  4sqlem2  12745  4sqlem3  12746  4sqlem4  12748  mul4sqlem  12749  4sqlem11  12757  4sqlem16  12762  4sqlem17  12763  4sqlem19  12765  setscomd  12906  ressvalsets  12929  strressid  12936  ressval3d  12937  ressinbasd  12939  ressressg  12940  ressabsg  12941  grpinvalem  13250  grpinva  13251  grprida  13252  isnsgrp  13271  sgrpass  13273  sgrp1  13276  sgrppropd  13278  prdssgrpd  13280  mnd32g  13292  mnd4g  13294  mndpropd  13305  prdsidlem  13312  prdsmndd  13313  imasmnd2  13317  mhmex  13327  mhmlin  13332  gsumwmhm  13363  grprcan  13402  grpsubval  13411  grpinvid2  13418  grpasscan2  13429  grpsubinv  13438  grpinvadd  13443  grpsubid1  13450  grpsubadd0sub  13452  grpsubadd  13453  grpsubsub  13454  grpaddsubass  13455  grppncan  13456  grpnnncan2  13462  grpsubpropd2  13470  imasgrp2  13479  mhmlem  13483  mhmid  13484  mhmmnd  13485  ghmgrp  13487  mulgnn0gsum  13497  mulgnnp1  13499  mulgaddcomlem  13514  mulgaddcom  13515  mulginvinv  13517  mulgnn0dir  13521  mulgdirlem  13522  mulgp1  13524  mulgneg2  13525  mulgnn0ass  13527  mulgass  13528  mulgmodid  13530  mulgsubdir  13531  nmzsubg  13579  0nsg  13583  eqger  13593  qussub  13606  ghmlin  13617  ghmsub  13620  conjghm  13645  ablsub4  13682  abladdsub4  13683  ablsubsub4  13688  ablsub32  13691  ablnnncan  13692  gsumfzmptfidmadd2  13709  gsumfzconst  13710  gsumfzmhm2  13713  gsumfzsnfd  13714  mgpress  13726  rngass  13734  rngdi  13735  rngdir  13736  rngrz  13741  rngmneg2  13743  rngsubdi  13746  rngsubdir  13747  rngpropd  13750  imasrng  13751  srgass  13766  srgpcomp  13785  srgpcompp  13786  srgpcomppsc  13787  srg1expzeq1  13790  ringpropd  13833  ringrz  13839  ringnegr  13847  ringmneg2  13849  ringsubdi  13851  ringsubdir  13852  ring1  13854  imasring  13859  opprrng  13872  opprring  13874  mulgass3  13880  dvdsrd  13889  unitgrp  13911  invrfvald  13917  dvr1  13933  dvrass  13934  dvrcan1  13935  dvrcan3  13936  rdivmuldivd  13939  subrginv  14032  subrgdv  14033  resrhm2b  14044  islmod  14086  lmodlema  14087  islmodd  14088  lmodvs0  14117  lmodvneg1  14125  lmodvsubval2  14137  lmodsubvs  14138  lmodsubdi  14139  lmodsubdir  14140  lmodprop2d  14143  rmodislmodlem  14145  rmodislmod  14146  lsssn0  14165  sraval  14232  cnfldsub  14370  gsumfzfsumlem0  14381  gsumfzfsumlemm  14382  mulgrhm  14404  mulgrhm2  14405  znval  14431  znval2  14433  znunit  14454  psrval  14461  mplvalcoe  14485  mplval2g  14490  restabs  14680  cnprcl2k  14711  cnrest2r  14742  ispsmet  14828  psmettri2  14833  psmetsym  14834  ismet  14849  isxmet  14850  xmettri2  14866  xmetsym  14873  xmettri3  14879  mettri3  14880  xblss2ps  14909  xblss2  14910  comet  15004  xmetxp  15012  xmetxpbl  15013  txmetcnp  15023  fsumcncntop  15072  cncfi  15083  divcncfap  15119  limccl  15164  ellimc3apf  15165  limccnpcntop  15180  limccnp2lem  15181  reldvg  15184  dvfvalap  15186  eldvap  15187  dvcj  15214  dvfre  15215  dvexp  15216  dvexp2  15217  dvrecap  15218  dvmptaddx  15224  dvmptmulx  15225  dvmptnegcn  15227  dvmptsubcn  15228  dvmptcjx  15229  dvmptfsum  15230  dveflem  15231  dvef  15232  plyconst  15250  plyaddlem1  15252  plymullem1  15253  plyadd  15256  plymul  15257  plycoeid3  15262  plycolemc  15263  plyco  15264  plycjlemc  15265  plycj  15266  plyrecj  15268  dvply1  15270  dvply2g  15271  sin0pilem1  15286  sin0pilem2  15287  efper  15312  sinperlem  15313  efimpi  15324  ptolemy  15329  tangtx  15343  abssinper  15351  cosq34lt1  15355  rpcxpef  15399  rpcxpp1  15411  rpcxpneg  15412  rpcxpsub  15413  rpmulcxp  15414  rpdivcxp  15416  cxpmul  15417  rpcxpmul2  15418  rpcxproot  15419  cxpcom  15443  rpabscxpbnd  15445  rplogbval  15450  rplogbreexp  15458  rplogbzexp  15459  rprelogbmulexp  15461  rprelogbdiv  15462  relogbexpap  15463  rplogbcxp  15468  rpcxplogb  15469  logbgcd1irr  15472  logbgcd1irraplemap  15474  binom4  15484  wilthlem1  15485  sgmval  15488  sgmppw  15497  1sgmprm  15499  mersenne  15502  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgslem1  15510  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsval4  15530  lgsneg  15534  lgsneg1  15535  lgsmod  15536  lgsdir2  15543  lgsdirprm  15544  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgssq2  15551  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem2  15572  gausslemma2dlem3  15573  gausslemma2dlem4  15574  gausslemma2dlem5  15576  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  lgsquad2lem2  15592  lgsquad2  15593  lgsquad3  15594  m1lgs  15595  2lgslem3c  15605  2lgslem3d  15606  2lgslem3d1  15610  2sqlem2  15625  2sqlem3  15627  2sqlem4  15628  2sqlem8  15633  2sqlem9  15634  2sqlem10  15635  qdencn  16003  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trilpo  16019  apdifflemf  16022  apdiff  16024  iswomni0  16027  redcwlpolemeq1  16030  redcwlpo  16031  nconstwlpolem0  16039  nconstwlpolemgt0  16040  nconstwlpo  16042  neapmkv  16044