Theorem oveq12d 6019

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 6010	. 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 6001

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 6004

This theorem is referenced by:  oveq123d  6022  ovmpodxf  6130  ovmpodf  6136  caovdig  6180  caovdir2d  6182  caovdirg  6183  caovdilemd  6197  caovlem2d  6198  offval  6226  ofvalg  6228  offval2  6234  ofco  6237  caofinvl  6244  offres  6280  nnmsucr  6634  nndir  6636  ecovdi  6793  ecovidi  6794  dfplpq2  7541  dfmpq2  7542  addcmpblnq  7554  mulpipqqs  7560  addassnqg  7569  distrnqg  7574  ltaddnq  7594  halfnqq  7597  enq0tr  7621  addcmpblnq0  7630  addnq0mo  7634  addnnnq0  7636  nqnq0a  7641  distrnq0  7646  addassnq0  7649  distnq0r  7650  nq02m  7652  ltexpri  7800  cauappcvgprlemm  7832  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlem2  7847  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemmu  7882  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  caucvgprprlem2  7897  mulcmpblnrlemg  7927  mulsrmo  7931  mulsrpr  7933  mulcomsrg  7944  distrsrg  7946  recexgt0sr  7960  mulgt0sr  7965  mulextsr1lem  7967  caucvgsrlemgt1  7982  caucvgsr  7989  addcnsr  8021  mulcnsr  8022  recidpirqlemcalc  8044  axaddcl  8051  axmulcl  8053  axmulcom  8058  axmulass  8060  axdistr  8061  axcaucvglemcau  8085  axcaucvglemres  8086  adddir  8137  muladd11  8279  1p1times  8280  muladd11r  8302  pnpcan2  8386  muladd  8530  subdir  8532  mulsub  8547  mulreim  8751  apadd1  8755  mulext1  8759  recextlem1  8798  muleqadd  8815  divdirap  8844  divadddivap  8874  conjmulap  8876  divcanap5rd  8965  subrecap  8986  xp1d2m1eqxm1d2  9364  div4p1lem1div2  9365  cnref1o  9846  xnegid  10055  xposdif  10078  xleaddadd  10083  icoshftf1o  10187  lincmb01cmp  10199  iccf1o  10200  fz01en  10249  fzrev3  10283  fzrevral2  10302  fzrevral3  10303  fzshftral  10304  fzoaddel2  10396  fzosubel  10400  fzosubel2  10401  fzocatel  10405  modqsubdir  10615  addmodlteq  10620  frecuzrdgsuc  10636  frecfzen2  10649  iseqovex  10680  seqvalcd  10683  seq3caopr3  10713  seqcaopr3g  10714  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seqf1oglem2  10742  seq3id3  10746  seqfeq3  10751  seq3distr  10754  ser3le  10759  mulexp  10800  mulexpzap  10801  expaddzap  10805  expubnd  10818  subsq  10868  binom2  10873  binom21  10874  binom2sub  10875  binom2sub1  10876  binom3  10879  sqoddm1div8  10915  mulsubdivbinom2ap  10933  nn0opthlem1d  10942  nn0opthd  10944  facp1  10952  facubnd  10967  bcval  10971  bcn1  10980  bcm1k  10982  bcp1n  10983  bcp1nk  10984  bcval5  10985  bcn2  10986  bcpasc  10988  hashun  11027  hashfz  11043  ccatlid  11141  ccatass  11143  ccat1st1st  11172  swrdval  11180  swrdspsleq  11199  ccatswrd  11202  pfxval  11206  addlenpfx  11223  ccatpfx  11233  ccatopth  11248  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12  11265  swrdccat  11267  swrdccat3blem  11271  swrdccatin2d  11276  pfxccatin12d  11277  cats1lend  11299  cats2catd  11301  s2eqd  11302  s3eqd  11303  s4eqd  11304  s5eqd  11305  s6eqd  11306  s7eqd  11307  s8eqd  11308  crre  11368  replim  11370  remullem  11382  remul2  11384  immul2  11391  cjcj  11394  cjadd  11395  ipcnval  11397  cjmulval  11399  cjneg  11401  imval2  11405  cjreim  11414  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemp1rp  11517  resqrexlemfp1  11520  resqrexlemcalc1  11525  resqrexlemcalc2  11526  resqrex  11537  sqabsadd  11566  sqabssub  11567  absreimsq  11578  recan  11620  amgm2  11629  maxabslemab  11717  maxabslemval  11719  max0addsup  11730  minabs  11747  bdtrilem  11750  bdtri  11751  xrmaxadd  11772  xrminadd  11786  xrbdtri  11787  subcn2  11822  reccn2ap  11824  climle  11845  climcvg1nlem  11860  serf0  11863  fsumadd  11917  fsumsplit  11918  sumpr  11924  sumtp  11925  isumadd  11942  sumsplitdc  11943  fsum2dlemstep  11945  fsumshftm  11956  fisumrev2  11957  fsumconst  11965  modfsummodlemstep  11968  telfsumo  11977  fsumparts  11981  binomlem  11994  binom  11995  binom1dif  11998  bcxmaslem1  11999  isumsplit  12002  isumnn0nn  12004  arisum  12009  arisum2  12010  trireciplem  12011  trirecip  12012  geosergap  12017  geo2sum  12025  geo2sum2  12026  cvgratnnlemsumlt  12039  mertenslemi1  12046  mertensabs  12048  fprodmul  12102  fprodsplitdc  12107  fprodabs  12127  fprod2dlemstep  12133  fproddivapf  12142  eftabs  12167  eftvalcn  12168  efcllemp  12169  ege2le3  12182  efcj  12184  efaddlem  12185  efsep  12202  ef4p  12205  efgt1p2  12206  efgt1p  12207  sinval  12213  cosval  12214  tanvalap  12219  tanval2ap  12224  tanval3ap  12225  efi4p  12228  sinneg  12237  cosneg  12238  tannegap  12239  efival  12243  efmival  12244  sinadd  12247  cosadd  12248  tanaddaplem  12249  tanaddap  12250  sinsub  12251  cossub  12252  addsin  12253  subsin  12254  sinmul  12255  cosmul  12256  addcos  12257  subcos  12258  sincossq  12259  cos2t  12261  sin01bnd  12268  cos01bnd  12269  efieq1re  12283  demoivreALT  12285  dvds2ln  12335  odd2np1lem  12383  bitsinv1lem  12472  gcdaddm  12505  bezoutlemnewy  12517  dfgcd3  12531  dvdsgcd  12533  mulgcd  12537  mulgcdr  12539  gcddiv  12540  sqgcd  12550  lcmgcdlem  12599  lcmgcd  12600  qredeu  12619  divgcdcoprm0  12623  cncongr1  12625  oddpwdclemdc  12695  sqrt2irraplemnn  12701  qnumdenbi  12714  zgcdsq  12723  hashdvds  12743  phiprmpw  12744  phimullem  12747  eulerthlema  12752  prmdiv  12757  modprm0  12777  coprimeprodsq  12780  pythagtriplem1  12788  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem15  12801  pythagtriplem16  12802  pythagtriplem17  12803  pythagtriplem19  12805  pcval  12819  pcmul  12824  pcdiv  12825  pcqmul  12826  pcid  12847  pcaddlem  12862  pcmpt  12866  pcmpt2  12867  pcmptdvds  12868  pcbc  12874  4sqlem4  12915  mul4sqlem  12916  mul4sq  12917  4sqlem11  12924  4sqlem12  12925  4sqlem15  12928  4sqlem17  12930  ennnfonelemp1  12977  nninfdclemp1  13021  ressvalsets  13097  topnvalg  13284  topnpropgd  13286  prdsex  13302  prdsval  13306  pwsval  13324  qusval  13356  qusex  13358  qusaddvallemg  13366  xpsval  13385  gsumprval  13432  imasmnd2  13485  ismhm  13494  mhmf1o  13503  0mhm  13519  mhmco  13523  mhmeql  13525  gsumfzz  13528  isgrpid2  13573  grpnpcan  13625  imasgrp2  13647  mhmmnd  13653  mulgnndir  13688  mulgdir  13691  isnsg3  13744  isghm  13780  ghmnsgima  13805  ghmf1o  13812  conjghm  13813  qusghm  13819  ablsub4  13850  ghmcmn  13864  invghm  13866  gsumfzmptfidmadd  13876  gsumfzconst  13878  mgpvalg  13886  mgptopng  13892  mgpress  13894  rngdi  13903  rngdir  13904  rngpropd  13918  imasrng  13919  srglmhm  13956  srgrmhm  13957  ringo2times  13991  ringcom  13994  ringpropd  14001  ring1  14022  ringlghm  14024  ringrghm  14025  imasring  14027  opprvalg  14032  opprrng  14040  opprring  14042  invrfvald  14086  dvrvald  14098  dvrdir  14107  rdivmuldivd  14108  islmod  14255  lmodlema  14256  islmodd  14257  lmodcom  14297  lmodnegadd  14300  lmodprop2d  14312  rmodislmod  14315  lsssn0  14334  sraval  14401  qusrhm  14492  gsumfzfsumlemm  14551  expghmap  14571  mulgghm2  14572  mulgrhm  14573  zlmval  14591  znval  14600  psrval  14630  mplvalcoe  14654  cnfval  14868  cnpfval  14869  ispsmet  14997  psmet0  15001  psmettri2  15002  psmetres2  15007  ismet  15018  isxmet  15019  xmettri2  15035  xmetres2  15053  xblss2  15079  xmstri2  15144  mstri2  15145  xmstri  15146  mstri  15147  xmstri3  15148  mstri3  15149  msrtri  15150  comet  15173  bdxmet  15175  txmetcnp  15192  metcnpd  15194  cnmet  15204  ioo2bl  15225  mpomulcn  15240  fsumcncntop  15241  elcncf  15247  mulc1cncf  15263  cncfco  15265  cncfcncntop  15267  cncfmptc  15270  cncfmptid  15271  addccncf  15274  cdivcncfap  15278  negcncf  15279  mulcncflem  15281  limccnp2cntop  15351  reldvg  15353  dvfvalap  15355  eldvap  15356  dvconst  15368  dvconstre  15370  dvconstss  15372  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvexp  15385  dvrecap  15387  dvmptid  15390  dvmptc  15391  dveflem  15400  dvef  15401  elplyd  15415  ply1termlem  15416  plyaddlem1  15421  plymullem1  15422  plyadd  15425  plymul  15426  plycoeid3  15431  plycolemc  15432  plyco  15433  plycjlemc  15434  plycj  15435  plyrecj  15437  dvply1  15439  dvply2g  15440  sinperlem  15482  sinmpi  15489  cosmpi  15490  sinppi  15491  cosppi  15492  efimpi  15493  sinhalfpip  15494  sinhalfpim  15495  coshalfpip  15496  coshalfpim  15497  ptolemy  15498  tangtx  15512  logdivlti  15555  rpcxpadd  15579  rpmulcxp  15583  rplogbchbase  15624  rprelogbmul  15629  binom4  15653  wilthlem1  15654  1sgmprm  15668  1sgm2ppw  15669  sgmmul  15670  mersenne  15671  perfect1  15672  perfectlem2  15674  perfect  15675  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsval4a  15701  lgsneg  15703  lgsdilem  15706  lgsdirprm  15713  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  gausslemma2dlem4  15743  gausslemma2dlem6  15746  lgseisenlem2  15750  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem1  15760  lgsquad2lem2  15761  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2sqlem2  15794  2sqlem3  15796  2sqlem4  15797  2sqlem8  15802  cvgcmp2nlemabs  16400  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trilpo  16411  redcwlpo  16423  nconstwlpolemgt0  16432  nconstwlpo  16434  neapmkv  16436