Theorem oveq12d 6025

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 6016	. 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 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq123d  6028  ovmpodxf  6136  ovmpodf  6142  caovdig  6186  caovdir2d  6188  caovdirg  6189  caovdilemd  6203  caovlem2d  6204  offval  6232  ofvalg  6234  offval2  6240  ofco  6243  caofinvl  6250  offres  6286  nnmsucr  6642  nndir  6644  ecovdi  6801  ecovidi  6802  dfplpq2  7552  dfmpq2  7553  addcmpblnq  7565  mulpipqqs  7571  addassnqg  7580  distrnqg  7585  ltaddnq  7605  halfnqq  7608  enq0tr  7632  addcmpblnq0  7641  addnq0mo  7645  addnnnq0  7647  nqnq0a  7652  distrnq0  7657  addassnq0  7660  distnq0r  7661  nq02m  7663  ltexpri  7811  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemmu  7893  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem2  7908  mulcmpblnrlemg  7938  mulsrmo  7942  mulsrpr  7944  mulcomsrg  7955  distrsrg  7957  recexgt0sr  7971  mulgt0sr  7976  mulextsr1lem  7978  caucvgsrlemgt1  7993  caucvgsr  8000  addcnsr  8032  mulcnsr  8033  recidpirqlemcalc  8055  axaddcl  8062  axmulcl  8064  axmulcom  8069  axmulass  8071  axdistr  8072  axcaucvglemcau  8096  axcaucvglemres  8097  adddir  8148  muladd11  8290  1p1times  8291  muladd11r  8313  pnpcan2  8397  muladd  8541  subdir  8543  mulsub  8558  mulreim  8762  apadd1  8766  mulext1  8770  recextlem1  8809  muleqadd  8826  divdirap  8855  divadddivap  8885  conjmulap  8887  divcanap5rd  8976  subrecap  8997  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  cnref1o  9858  xnegid  10067  xposdif  10090  xleaddadd  10095  icoshftf1o  10199  lincmb01cmp  10211  iccf1o  10212  fz01en  10261  fzrev3  10295  fzrevral2  10314  fzrevral3  10315  fzshftral  10316  fzoaddel2  10408  fzosubel  10412  fzosubel2  10413  fzocatel  10417  modqsubdir  10627  addmodlteq  10632  frecuzrdgsuc  10648  frecfzen2  10661  iseqovex  10692  seqvalcd  10695  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seqf1oglem2  10754  seq3id3  10758  seqfeq3  10763  seq3distr  10766  ser3le  10771  mulexp  10812  mulexpzap  10813  expaddzap  10817  expubnd  10830  subsq  10880  binom2  10885  binom21  10886  binom2sub  10887  binom2sub1  10888  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  nn0opthd  10956  facp1  10964  facubnd  10979  bcval  10983  bcn1  10992  bcm1k  10994  bcp1n  10995  bcp1nk  10996  bcval5  10997  bcn2  10998  bcpasc  11000  hashun  11039  hashfz  11056  ccatlid  11154  ccatass  11156  ccat1st1st  11188  swrdval  11196  swrdspsleq  11215  ccatswrd  11218  pfxval  11222  addlenpfx  11239  ccatpfx  11249  ccatopth  11264  pfxccatin12lem1  11276  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12  11281  swrdccat  11283  swrdccat3blem  11287  swrdccatin2d  11292  pfxccatin12d  11293  cats1lend  11315  cats2catd  11317  s2eqd  11318  s3eqd  11319  s4eqd  11320  s5eqd  11321  s6eqd  11322  s7eqd  11323  s8eqd  11324  crre  11384  replim  11386  remullem  11398  remul2  11400  immul2  11407  cjcj  11410  cjadd  11411  ipcnval  11413  cjmulval  11415  cjneg  11417  imval2  11421  cjreim  11430  cvg1nlemcau  11511  cvg1nlemres  11512  resqrexlemp1rp  11533  resqrexlemfp1  11536  resqrexlemcalc1  11541  resqrexlemcalc2  11542  resqrex  11553  sqabsadd  11582  sqabssub  11583  absreimsq  11594  recan  11636  amgm2  11645  maxabslemab  11733  maxabslemval  11735  max0addsup  11746  minabs  11763  bdtrilem  11766  bdtri  11767  xrmaxadd  11788  xrminadd  11802  xrbdtri  11803  subcn2  11838  reccn2ap  11840  climle  11861  climcvg1nlem  11876  serf0  11879  fsumadd  11933  fsumsplit  11934  sumpr  11940  sumtp  11941  isumadd  11958  sumsplitdc  11959  fsum2dlemstep  11961  fsumshftm  11972  fisumrev2  11973  fsumconst  11981  modfsummodlemstep  11984  telfsumo  11993  fsumparts  11997  binomlem  12010  binom  12011  binom1dif  12014  bcxmaslem1  12015  isumsplit  12018  isumnn0nn  12020  arisum  12025  arisum2  12026  trireciplem  12027  trirecip  12028  geosergap  12033  geo2sum  12041  geo2sum2  12042  cvgratnnlemsumlt  12055  mertenslemi1  12062  mertensabs  12064  fprodmul  12118  fprodsplitdc  12123  fprodabs  12143  fprod2dlemstep  12149  fproddivapf  12158  eftabs  12183  eftvalcn  12184  efcllemp  12185  ege2le3  12198  efcj  12200  efaddlem  12201  efsep  12218  ef4p  12221  efgt1p2  12222  efgt1p  12223  sinval  12229  cosval  12230  tanvalap  12235  tanval2ap  12240  tanval3ap  12241  efi4p  12244  sinneg  12253  cosneg  12254  tannegap  12255  efival  12259  efmival  12260  sinadd  12263  cosadd  12264  tanaddaplem  12265  tanaddap  12266  sinsub  12267  cossub  12268  addsin  12269  subsin  12270  sinmul  12271  cosmul  12272  addcos  12273  subcos  12274  sincossq  12275  cos2t  12277  sin01bnd  12284  cos01bnd  12285  efieq1re  12299  demoivreALT  12301  dvds2ln  12351  odd2np1lem  12399  bitsinv1lem  12488  gcdaddm  12521  bezoutlemnewy  12533  dfgcd3  12547  dvdsgcd  12549  mulgcd  12553  mulgcdr  12555  gcddiv  12556  sqgcd  12566  lcmgcdlem  12615  lcmgcd  12616  qredeu  12635  divgcdcoprm0  12639  cncongr1  12641  oddpwdclemdc  12711  sqrt2irraplemnn  12717  qnumdenbi  12730  zgcdsq  12739  hashdvds  12759  phiprmpw  12760  phimullem  12763  eulerthlema  12768  prmdiv  12773  modprm0  12793  coprimeprodsq  12796  pythagtriplem1  12804  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem15  12817  pythagtriplem16  12818  pythagtriplem17  12819  pythagtriplem19  12821  pcval  12835  pcmul  12840  pcdiv  12841  pcqmul  12842  pcid  12863  pcaddlem  12878  pcmpt  12882  pcmpt2  12883  pcmptdvds  12884  pcbc  12890  4sqlem4  12931  mul4sqlem  12932  mul4sq  12933  4sqlem11  12940  4sqlem12  12941  4sqlem15  12944  4sqlem17  12946  ennnfonelemp1  12993  nninfdclemp1  13037  ressvalsets  13113  topnvalg  13300  topnpropgd  13302  prdsex  13318  prdsval  13322  pwsval  13340  qusval  13372  qusex  13374  qusaddvallemg  13382  xpsval  13401  gsumprval  13448  imasmnd2  13501  ismhm  13510  mhmf1o  13519  0mhm  13535  mhmco  13539  mhmeql  13541  gsumfzz  13544  isgrpid2  13589  grpnpcan  13641  imasgrp2  13663  mhmmnd  13669  mulgnndir  13704  mulgdir  13707  isnsg3  13760  isghm  13796  ghmnsgima  13821  ghmf1o  13828  conjghm  13829  qusghm  13835  ablsub4  13866  ghmcmn  13880  invghm  13882  gsumfzmptfidmadd  13892  gsumfzconst  13894  mgpvalg  13902  mgptopng  13908  mgpress  13910  rngdi  13919  rngdir  13920  rngpropd  13934  imasrng  13935  srglmhm  13972  srgrmhm  13973  ringo2times  14007  ringcom  14010  ringpropd  14017  ring1  14038  ringlghm  14040  ringrghm  14041  imasring  14043  opprvalg  14048  opprrng  14056  opprring  14058  invrfvald  14102  dvrvald  14114  dvrdir  14123  rdivmuldivd  14124  islmod  14271  lmodlema  14272  islmodd  14273  lmodcom  14313  lmodnegadd  14316  lmodprop2d  14328  rmodislmod  14331  lsssn0  14350  sraval  14417  qusrhm  14508  gsumfzfsumlemm  14567  expghmap  14587  mulgghm2  14588  mulgrhm  14589  zlmval  14607  znval  14616  psrval  14646  mplvalcoe  14670  cnfval  14884  cnpfval  14885  ispsmet  15013  psmet0  15017  psmettri2  15018  psmetres2  15023  ismet  15034  isxmet  15035  xmettri2  15051  xmetres2  15069  xblss2  15095  xmstri2  15160  mstri2  15161  xmstri  15162  mstri  15163  xmstri3  15164  mstri3  15165  msrtri  15166  comet  15189  bdxmet  15191  txmetcnp  15208  metcnpd  15210  cnmet  15220  ioo2bl  15241  mpomulcn  15256  fsumcncntop  15257  elcncf  15263  mulc1cncf  15279  cncfco  15281  cncfcncntop  15283  cncfmptc  15286  cncfmptid  15287  addccncf  15290  cdivcncfap  15294  negcncf  15295  mulcncflem  15297  limccnp2cntop  15367  reldvg  15369  dvfvalap  15371  eldvap  15372  dvconst  15384  dvconstre  15386  dvconstss  15388  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvexp  15401  dvrecap  15403  dvmptid  15406  dvmptc  15407  dveflem  15416  dvef  15417  elplyd  15431  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plyadd  15441  plymul  15442  plycoeid3  15447  plycolemc  15448  plyco  15449  plycjlemc  15450  plycj  15451  plyrecj  15453  dvply1  15455  dvply2g  15456  sinperlem  15498  sinmpi  15505  cosmpi  15506  sinppi  15507  cosppi  15508  efimpi  15509  sinhalfpip  15510  sinhalfpim  15511  coshalfpip  15512  coshalfpim  15513  ptolemy  15514  tangtx  15528  logdivlti  15571  rpcxpadd  15595  rpmulcxp  15599  rplogbchbase  15640  rprelogbmul  15645  binom4  15669  wilthlem1  15670  1sgmprm  15684  1sgm2ppw  15685  sgmmul  15686  mersenne  15687  perfect1  15688  perfectlem2  15690  perfect  15691  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsval4a  15717  lgsneg  15719  lgsdilem  15722  lgsdirprm  15729  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  gausslemma2dlem4  15759  gausslemma2dlem6  15762  lgseisenlem2  15766  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem1  15776  lgsquad2lem2  15777  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2sqlem2  15810  2sqlem3  15812  2sqlem4  15813  2sqlem8  15818  vtxdgfval  16048  vtxdgfifival  16051  vtxdgop  16052  vtxdgfi0e  16055  vtxdeqd  16056  vtxdfifiun  16057  vtxduspgrfvedgfi  16061  cvgcmp2nlemabs  16488  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trilpo  16499  redcwlpo  16511  nconstwlpolemgt0  16520  nconstwlpo  16522  neapmkv  16524