Theorem oveq12d 5859

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 5850	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   = wceq 1343  (class class class)co 5841

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  oveq123d  5862  ovmpodxf  5963  ovmpodf  5969  caovdig  6012  caovdir2d  6014  caovdirg  6015  caovdilemd  6029  caovlem2d  6030  offval  6056  ofvalg  6058  offval2  6064  ofco  6067  caofinvl  6071  offres  6100  nnmsucr  6452  nndir  6454  ecovdi  6608  ecovidi  6609  dfplpq2  7291  dfmpq2  7292  addcmpblnq  7304  mulpipqqs  7310  addassnqg  7319  distrnqg  7324  ltaddnq  7344  halfnqq  7347  enq0tr  7371  addcmpblnq0  7380  addnq0mo  7384  addnnnq0  7386  nqnq0a  7391  distrnq0  7396  addassnq0  7399  distnq0r  7400  nq02m  7402  ltexpri  7550  cauappcvgprlemm  7582  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem2  7617  caucvgpr  7619  caucvgprprlemelu  7623  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemmu  7632  caucvgprprlemopu  7636  caucvgprprlemloc  7640  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  caucvgprprlem2  7647  mulcmpblnrlemg  7677  mulsrmo  7681  mulsrpr  7683  mulcomsrg  7694  distrsrg  7696  recexgt0sr  7710  mulgt0sr  7715  mulextsr1lem  7717  caucvgsrlemgt1  7732  caucvgsr  7739  addcnsr  7771  mulcnsr  7772  recidpirqlemcalc  7794  axaddcl  7801  axmulcl  7803  axmulcom  7808  axmulass  7810  axdistr  7811  axcaucvglemcau  7835  axcaucvglemres  7836  adddir  7886  muladd11  8027  1p1times  8028  muladd11r  8050  pnpcan2  8134  muladd  8278  subdir  8280  mulsub  8295  mulreim  8498  apadd1  8502  mulext1  8506  recextlem1  8544  muleqadd  8561  divdirap  8589  divadddivap  8619  conjmulap  8621  divcanap5rd  8710  subrecap  8731  xp1d2m1eqxm1d2  9105  div4p1lem1div2  9106  cnref1o  9584  xnegid  9791  xposdif  9814  xleaddadd  9819  icoshftf1o  9923  lincmb01cmp  9935  iccf1o  9936  fz01en  9984  fzrev3  10018  fzrevral2  10037  fzrevral3  10038  fzshftral  10039  fzoaddel2  10124  fzosubel  10125  fzosubel2  10126  fzocatel  10130  modqsubdir  10324  addmodlteq  10329  frecuzrdgsuc  10345  frecfzen2  10358  iseqovex  10387  seqvalcd  10390  seq3caopr3  10412  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3id3  10438  seqfeq3  10443  seq3distr  10444  ser3le  10449  mulexp  10490  mulexpzap  10491  expaddzap  10495  expubnd  10508  subsq  10557  binom2  10562  binom21  10563  binom2sub  10564  binom2sub1  10565  binom3  10568  sqoddm1div8  10604  nn0opthlem1d  10629  nn0opthd  10631  facp1  10639  facubnd  10654  bcval  10658  bcn1  10667  bcm1k  10669  bcp1n  10670  bcp1nk  10671  bcval5  10672  bcn2  10673  bcpasc  10675  hashun  10714  hashfz  10730  crre  10795  replim  10797  remullem  10809  remul2  10811  immul2  10818  cjcj  10821  cjadd  10822  ipcnval  10824  cjmulval  10826  cjneg  10828  imval2  10832  cjreim  10841  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrexlemcalc1  10952  resqrexlemcalc2  10953  resqrex  10964  sqabsadd  10993  sqabssub  10994  absreimsq  11005  recan  11047  amgm2  11056  maxabslemab  11144  maxabslemval  11146  max0addsup  11157  minabs  11173  bdtrilem  11176  bdtri  11177  xrmaxadd  11198  xrminadd  11212  xrbdtri  11213  subcn2  11248  reccn2ap  11250  climle  11271  climcvg1nlem  11286  serf0  11289  fsumadd  11343  fsumsplit  11344  sumpr  11350  sumtp  11351  isumadd  11368  sumsplitdc  11369  fsum2dlemstep  11371  fsumshftm  11382  fisumrev2  11383  fsumconst  11391  modfsummodlemstep  11394  telfsumo  11403  fsumparts  11407  binomlem  11420  binom  11421  binom1dif  11424  bcxmaslem1  11425  isumsplit  11428  isumnn0nn  11430  arisum  11435  arisum2  11436  trireciplem  11437  trirecip  11438  geosergap  11443  geo2sum  11451  geo2sum2  11452  cvgratnnlemsumlt  11465  mertenslemi1  11472  mertensabs  11474  fprodmul  11528  fprodsplitdc  11533  fprodabs  11553  fprod2dlemstep  11559  fproddivapf  11568  eftabs  11593  eftvalcn  11594  efcllemp  11595  ege2le3  11608  efcj  11610  efaddlem  11611  efsep  11628  ef4p  11631  efgt1p2  11632  efgt1p  11633  sinval  11639  cosval  11640  tanvalap  11645  tanval2ap  11650  tanval3ap  11651  efi4p  11654  sinneg  11663  cosneg  11664  tannegap  11665  efival  11669  efmival  11670  sinadd  11673  cosadd  11674  tanaddaplem  11675  tanaddap  11676  sinsub  11677  cossub  11678  addsin  11679  subsin  11680  sinmul  11681  cosmul  11682  addcos  11683  subcos  11684  sincossq  11685  cos2t  11687  sin01bnd  11694  cos01bnd  11695  efieq1re  11708  demoivreALT  11710  dvds2ln  11760  odd2np1lem  11805  gcdaddm  11913  bezoutlemnewy  11925  dfgcd3  11939  dvdsgcd  11941  mulgcd  11945  mulgcdr  11947  gcddiv  11948  sqgcd  11958  lcmgcdlem  12005  lcmgcd  12006  qredeu  12025  divgcdcoprm0  12029  cncongr1  12031  oddpwdclemdc  12101  sqrt2irraplemnn  12107  qnumdenbi  12120  zgcdsq  12129  hashdvds  12149  phiprmpw  12150  phimullem  12153  eulerthlema  12158  prmdiv  12163  modprm0  12182  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  pythagtriplem19  12210  pcval  12224  pcmul  12229  pcdiv  12230  pcqmul  12231  pcid  12251  pcaddlem  12266  pcmpt  12269  pcmpt2  12270  pcmptdvds  12271  pcbc  12277  4sqlem4  12318  mul4sqlem  12319  mul4sq  12320  ennnfonelemp1  12335  nninfdclemp1  12379  ressid2  12449  ressval2  12450  topnvalg  12563  topnpropgd  12565  cnfval  12794  cnpfval  12795  ispsmet  12923  psmet0  12927  psmettri2  12928  psmetres2  12933  ismet  12944  isxmet  12945  xmettri2  12961  xmetres2  12979  xblss2  13005  xmstri2  13070  mstri2  13071  xmstri  13072  mstri  13073  xmstri3  13074  mstri3  13075  msrtri  13076  comet  13099  bdxmet  13101  txmetcnp  13118  metcnpd  13120  cnmet  13130  ioo2bl  13143  fsumcncntop  13156  elcncf  13160  mulc1cncf  13176  cncfco  13178  cncfcncntop  13180  cncfmptc  13182  cncfmptid  13183  addccncf  13186  cdivcncfap  13187  negcncf  13188  mulcncflem  13190  limccnp2cntop  13246  reldvg  13248  dvfvalap  13250  eldvap  13251  dvconst  13261  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvexp  13275  dvrecap  13277  dveflem  13287  dvef  13288  sinperlem  13329  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  efimpi  13340  sinhalfpip  13341  sinhalfpim  13342  coshalfpip  13343  coshalfpim  13344  ptolemy  13345  tangtx  13359  logdivlti  13402  rpcxpadd  13426  rpmulcxp  13430  rplogbchbase  13468  rprelogbmul  13473  binom4  13497  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsval4a  13523  lgsneg  13525  lgsdilem  13528  lgsdirprm  13535  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  2sqlem2  13551  2sqlem3  13553  2sqlem4  13554  2sqlem8  13559  cvgcmp2nlemabs  13871  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trilpo  13882  redcwlpo  13894  nconstwlpolemgt0  13902  nconstwlpo  13904  neapmkv  13906