Theorem oveq12d 6036

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
oveq1d.1	|- ( ph -> A = B )
oveq12d.2	|- ( ph -> C = D )

Assertion

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

Proof of Theorem oveq12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq12d.2	. 2 |- ( ph -> C = D )
3		oveq12 6027	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq123d  6039  ovmpodxf  6147  ovmpodf  6153  caovdig  6197  caovdir2d  6199  caovdirg  6200  caovdilemd  6214  caovlem2d  6215  offval  6243  ofvalg  6245  offval2  6251  ofco  6254  caofinvl  6261  offres  6297  nnmsucr  6656  nndir  6658  ecovdi  6815  ecovidi  6816  dfplpq2  7574  dfmpq2  7575  addcmpblnq  7587  mulpipqqs  7593  addassnqg  7602  distrnqg  7607  ltaddnq  7627  halfnqq  7630  enq0tr  7654  addcmpblnq0  7663  addnq0mo  7667  addnnnq0  7669  nqnq0a  7674  distrnq0  7679  addassnq0  7682  distnq0r  7683  nq02m  7685  ltexpri  7833  cauappcvgprlemm  7865  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemmu  7915  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem2  7930  mulcmpblnrlemg  7960  mulsrmo  7964  mulsrpr  7966  mulcomsrg  7977  distrsrg  7979  recexgt0sr  7993  mulgt0sr  7998  mulextsr1lem  8000  caucvgsrlemgt1  8015  caucvgsr  8022  addcnsr  8054  mulcnsr  8055  recidpirqlemcalc  8077  axaddcl  8084  axmulcl  8086  axmulcom  8091  axmulass  8093  axdistr  8094  axcaucvglemcau  8118  axcaucvglemres  8119  adddir  8170  muladd11  8312  1p1times  8313  muladd11r  8335  pnpcan2  8419  muladd  8563  subdir  8565  mulsub  8580  mulreim  8784  apadd1  8788  mulext1  8792  recextlem1  8831  muleqadd  8848  divdirap  8877  divadddivap  8907  conjmulap  8909  divcanap5rd  8998  subrecap  9019  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  cnref1o  9885  xnegid  10094  xposdif  10117  xleaddadd  10122  icoshftf1o  10226  lincmb01cmp  10238  iccf1o  10239  fz01en  10288  fzrev3  10322  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzoaddel2  10436  fzosubel  10440  fzosubel2  10441  fzocatel  10445  modqsubdir  10656  addmodlteq  10661  frecuzrdgsuc  10677  frecfzen2  10690  iseqovex  10721  seqvalcd  10724  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seqf1oglem2  10783  seq3id3  10787  seqfeq3  10792  seq3distr  10795  ser3le  10800  mulexp  10841  mulexpzap  10842  expaddzap  10846  expubnd  10859  subsq  10909  binom2  10914  binom21  10915  binom2sub  10916  binom2sub1  10917  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  nn0opthd  10985  facp1  10993  facubnd  11008  bcval  11012  bcn1  11021  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcn2  11027  bcpasc  11029  hashun  11069  hashfz  11086  hashtpgim  11110  ccatlid  11187  ccatass  11189  ccat1st1st  11222  swrdval  11233  swrdspsleq  11252  ccatswrd  11255  pfxval  11259  addlenpfx  11276  ccatpfx  11286  ccatopth  11301  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat  11320  swrdccat3blem  11324  swrdccatin2d  11329  pfxccatin12d  11330  cats1lend  11352  cats2catd  11354  s2eqd  11355  s3eqd  11356  s4eqd  11357  s5eqd  11358  s6eqd  11359  s7eqd  11360  s8eqd  11361  crre  11435  replim  11437  remullem  11449  remul2  11451  immul2  11458  cjcj  11461  cjadd  11462  ipcnval  11464  cjmulval  11466  cjneg  11468  imval2  11472  cjreim  11481  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrex  11604  sqabsadd  11633  sqabssub  11634  absreimsq  11645  recan  11687  amgm2  11696  maxabslemab  11784  maxabslemval  11786  max0addsup  11797  minabs  11814  bdtrilem  11817  bdtri  11818  xrmaxadd  11839  xrminadd  11853  xrbdtri  11854  subcn2  11889  reccn2ap  11891  climle  11912  climcvg1nlem  11927  serf0  11930  fsumadd  11985  fsumsplit  11986  sumpr  11992  sumtp  11993  isumadd  12010  sumsplitdc  12011  fsum2dlemstep  12013  fsumshftm  12024  fisumrev2  12025  fsumconst  12033  modfsummodlemstep  12036  telfsumo  12045  fsumparts  12049  binomlem  12062  binom  12063  binom1dif  12066  bcxmaslem1  12067  isumsplit  12070  isumnn0nn  12072  arisum  12077  arisum2  12078  trireciplem  12079  trirecip  12080  geosergap  12085  geo2sum  12093  geo2sum2  12094  cvgratnnlemsumlt  12107  mertenslemi1  12114  mertensabs  12116  fprodmul  12170  fprodsplitdc  12175  fprodabs  12195  fprod2dlemstep  12201  fproddivapf  12210  eftabs  12235  eftvalcn  12236  efcllemp  12237  ege2le3  12250  efcj  12252  efaddlem  12253  efsep  12270  ef4p  12273  efgt1p2  12274  efgt1p  12275  sinval  12281  cosval  12282  tanvalap  12287  tanval2ap  12292  tanval3ap  12293  efi4p  12296  sinneg  12305  cosneg  12306  tannegap  12307  efival  12311  efmival  12312  sinadd  12315  cosadd  12316  tanaddaplem  12317  tanaddap  12318  sinsub  12319  cossub  12320  addsin  12321  subsin  12322  sinmul  12323  cosmul  12324  addcos  12325  subcos  12326  sincossq  12327  cos2t  12329  sin01bnd  12336  cos01bnd  12337  efieq1re  12351  demoivreALT  12353  dvds2ln  12403  odd2np1lem  12451  bitsinv1lem  12540  gcdaddm  12573  bezoutlemnewy  12585  dfgcd3  12599  dvdsgcd  12601  mulgcd  12605  mulgcdr  12607  gcddiv  12608  sqgcd  12618  lcmgcdlem  12667  lcmgcd  12668  qredeu  12687  divgcdcoprm0  12691  cncongr1  12693  oddpwdclemdc  12763  sqrt2irraplemnn  12769  qnumdenbi  12782  zgcdsq  12791  hashdvds  12811  phiprmpw  12812  phimullem  12815  eulerthlema  12820  prmdiv  12825  modprm0  12845  coprimeprodsq  12848  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  pythagtriplem19  12873  pcval  12887  pcmul  12892  pcdiv  12893  pcqmul  12894  pcid  12915  pcaddlem  12930  pcmpt  12934  pcmpt2  12935  pcmptdvds  12936  pcbc  12942  4sqlem4  12983  mul4sqlem  12984  mul4sq  12985  4sqlem11  12992  4sqlem12  12993  4sqlem15  12996  4sqlem17  12998  ennnfonelemp1  13045  nninfdclemp1  13089  ressvalsets  13165  topnvalg  13352  topnpropgd  13354  prdsex  13370  prdsval  13374  pwsval  13392  qusval  13424  qusex  13426  qusaddvallemg  13434  xpsval  13453  gsumprval  13500  imasmnd2  13553  ismhm  13562  mhmf1o  13571  0mhm  13587  mhmco  13591  mhmeql  13593  gsumfzz  13596  isgrpid2  13641  grpnpcan  13693  imasgrp2  13715  mhmmnd  13721  mulgnndir  13756  mulgdir  13759  isnsg3  13812  isghm  13848  ghmnsgima  13873  ghmf1o  13880  conjghm  13881  qusghm  13887  ablsub4  13918  ghmcmn  13932  invghm  13934  gsumfzmptfidmadd  13944  gsumfzconst  13946  mgpvalg  13955  mgptopng  13961  mgpress  13963  rngdi  13972  rngdir  13973  rngpropd  13987  imasrng  13988  srglmhm  14025  srgrmhm  14026  ringo2times  14060  ringcom  14063  ringpropd  14070  ring1  14091  ringlghm  14093  ringrghm  14094  imasring  14096  opprvalg  14101  opprrng  14109  opprring  14111  invrfvald  14155  dvrvald  14167  dvrdir  14176  rdivmuldivd  14177  islmod  14324  lmodlema  14325  islmodd  14326  lmodcom  14366  lmodnegadd  14369  lmodprop2d  14381  rmodislmod  14384  lsssn0  14403  sraval  14470  qusrhm  14561  gsumfzfsumlemm  14620  expghmap  14640  mulgghm2  14641  mulgrhm  14642  zlmval  14660  znval  14669  psrval  14699  mplvalcoe  14723  cnfval  14937  cnpfval  14938  ispsmet  15066  psmet0  15070  psmettri2  15071  psmetres2  15076  ismet  15087  isxmet  15088  xmettri2  15104  xmetres2  15122  xblss2  15148  xmstri2  15213  mstri2  15214  xmstri  15215  mstri  15216  xmstri3  15217  mstri3  15218  msrtri  15219  comet  15242  bdxmet  15244  txmetcnp  15261  metcnpd  15263  cnmet  15273  ioo2bl  15294  mpomulcn  15309  fsumcncntop  15310  elcncf  15316  mulc1cncf  15332  cncfco  15334  cncfcncntop  15336  cncfmptc  15339  cncfmptid  15340  addccncf  15343  cdivcncfap  15347  negcncf  15348  mulcncflem  15350  limccnp2cntop  15420  reldvg  15422  dvfvalap  15424  eldvap  15425  dvconst  15437  dvconstre  15439  dvconstss  15441  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvexp  15454  dvrecap  15456  dvmptid  15459  dvmptc  15460  dveflem  15469  dvef  15470  elplyd  15484  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plyadd  15494  plymul  15495  plycoeid3  15500  plycolemc  15501  plyco  15502  plycjlemc  15503  plycj  15504  plyrecj  15506  dvply1  15508  dvply2g  15509  sinperlem  15551  sinmpi  15558  cosmpi  15559  sinppi  15560  cosppi  15561  efimpi  15562  sinhalfpip  15563  sinhalfpim  15564  coshalfpip  15565  coshalfpim  15566  ptolemy  15567  tangtx  15581  logdivlti  15624  rpcxpadd  15648  rpmulcxp  15652  rplogbchbase  15693  rprelogbmul  15698  binom4  15722  wilthlem1  15723  1sgmprm  15737  1sgm2ppw  15738  sgmmul  15739  mersenne  15740  perfect1  15741  perfectlem2  15743  perfect  15744  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsdilem  15775  lgsdirprm  15782  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem4  15812  gausslemma2dlem6  15815  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  lgsquad2lem2  15830  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2sqlem2  15863  2sqlem3  15865  2sqlem4  15866  2sqlem8  15871  vtxdgfval  16158  vtxdgfifival  16161  vtxdgop  16162  vtxdgfi0e  16165  vtxdeqd  16166  vtxdfifiun  16167  vtxduspgrfvedgfi  16171  1loopgrvd2fi  16175  cvgcmp2nlemabs  16687  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trilpo  16698  redcwlpo  16711  nconstwlpolemgt0  16720  nconstwlpo  16722  neapmkv  16724  gsumgfsum  16736  gfsump1  16738