Theorem oveq12d 5962

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 5953	. 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 1373  (class class class)co 5944

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 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveq123d  5965  ovmpodxf  6071  ovmpodf  6077  caovdig  6121  caovdir2d  6123  caovdirg  6124  caovdilemd  6138  caovlem2d  6139  offval  6166  ofvalg  6168  offval2  6174  ofco  6177  caofinvl  6184  offres  6220  nnmsucr  6574  nndir  6576  ecovdi  6733  ecovidi  6734  dfplpq2  7467  dfmpq2  7468  addcmpblnq  7480  mulpipqqs  7486  addassnqg  7495  distrnqg  7500  ltaddnq  7520  halfnqq  7523  enq0tr  7547  addcmpblnq0  7556  addnq0mo  7560  addnnnq0  7562  nqnq0a  7567  distrnq0  7572  addassnq0  7575  distnq0r  7576  nq02m  7578  ltexpri  7726  cauappcvgprlemm  7758  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlem2  7773  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemmu  7808  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem2  7823  mulcmpblnrlemg  7853  mulsrmo  7857  mulsrpr  7859  mulcomsrg  7870  distrsrg  7872  recexgt0sr  7886  mulgt0sr  7891  mulextsr1lem  7893  caucvgsrlemgt1  7908  caucvgsr  7915  addcnsr  7947  mulcnsr  7948  recidpirqlemcalc  7970  axaddcl  7977  axmulcl  7979  axmulcom  7984  axmulass  7986  axdistr  7987  axcaucvglemcau  8011  axcaucvglemres  8012  adddir  8063  muladd11  8205  1p1times  8206  muladd11r  8228  pnpcan2  8312  muladd  8456  subdir  8458  mulsub  8473  mulreim  8677  apadd1  8681  mulext1  8685  recextlem1  8724  muleqadd  8741  divdirap  8770  divadddivap  8800  conjmulap  8802  divcanap5rd  8891  subrecap  8912  xp1d2m1eqxm1d2  9290  div4p1lem1div2  9291  cnref1o  9772  xnegid  9981  xposdif  10004  xleaddadd  10009  icoshftf1o  10113  lincmb01cmp  10125  iccf1o  10126  fz01en  10175  fzrev3  10209  fzrevral2  10228  fzrevral3  10229  fzshftral  10230  fzoaddel2  10319  fzosubel  10323  fzosubel2  10324  fzocatel  10328  modqsubdir  10538  addmodlteq  10543  frecuzrdgsuc  10559  frecfzen2  10572  iseqovex  10603  seqvalcd  10606  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seqf1oglem2  10665  seq3id3  10669  seqfeq3  10674  seq3distr  10677  ser3le  10682  mulexp  10723  mulexpzap  10724  expaddzap  10728  expubnd  10741  subsq  10791  binom2  10796  binom21  10797  binom2sub  10798  binom2sub1  10799  binom3  10802  sqoddm1div8  10838  mulsubdivbinom2ap  10856  nn0opthlem1d  10865  nn0opthd  10867  facp1  10875  facubnd  10890  bcval  10894  bcn1  10903  bcm1k  10905  bcp1n  10906  bcp1nk  10907  bcval5  10908  bcn2  10909  bcpasc  10911  hashun  10950  hashfz  10966  ccatlid  11062  ccatass  11064  ccat1st1st  11093  swrdval  11101  swrdspsleq  11120  ccatswrd  11123  crre  11168  replim  11170  remullem  11182  remul2  11184  immul2  11191  cjcj  11194  cjadd  11195  ipcnval  11197  cjmulval  11199  cjneg  11201  imval2  11205  cjreim  11214  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemp1rp  11317  resqrexlemfp1  11320  resqrexlemcalc1  11325  resqrexlemcalc2  11326  resqrex  11337  sqabsadd  11366  sqabssub  11367  absreimsq  11378  recan  11420  amgm2  11429  maxabslemab  11517  maxabslemval  11519  max0addsup  11530  minabs  11547  bdtrilem  11550  bdtri  11551  xrmaxadd  11572  xrminadd  11586  xrbdtri  11587  subcn2  11622  reccn2ap  11624  climle  11645  climcvg1nlem  11660  serf0  11663  fsumadd  11717  fsumsplit  11718  sumpr  11724  sumtp  11725  isumadd  11742  sumsplitdc  11743  fsum2dlemstep  11745  fsumshftm  11756  fisumrev2  11757  fsumconst  11765  modfsummodlemstep  11768  telfsumo  11777  fsumparts  11781  binomlem  11794  binom  11795  binom1dif  11798  bcxmaslem1  11799  isumsplit  11802  isumnn0nn  11804  arisum  11809  arisum2  11810  trireciplem  11811  trirecip  11812  geosergap  11817  geo2sum  11825  geo2sum2  11826  cvgratnnlemsumlt  11839  mertenslemi1  11846  mertensabs  11848  fprodmul  11902  fprodsplitdc  11907  fprodabs  11927  fprod2dlemstep  11933  fproddivapf  11942  eftabs  11967  eftvalcn  11968  efcllemp  11969  ege2le3  11982  efcj  11984  efaddlem  11985  efsep  12002  ef4p  12005  efgt1p2  12006  efgt1p  12007  sinval  12013  cosval  12014  tanvalap  12019  tanval2ap  12024  tanval3ap  12025  efi4p  12028  sinneg  12037  cosneg  12038  tannegap  12039  efival  12043  efmival  12044  sinadd  12047  cosadd  12048  tanaddaplem  12049  tanaddap  12050  sinsub  12051  cossub  12052  addsin  12053  subsin  12054  sinmul  12055  cosmul  12056  addcos  12057  subcos  12058  sincossq  12059  cos2t  12061  sin01bnd  12068  cos01bnd  12069  efieq1re  12083  demoivreALT  12085  dvds2ln  12135  odd2np1lem  12183  bitsinv1lem  12272  gcdaddm  12305  bezoutlemnewy  12317  dfgcd3  12331  dvdsgcd  12333  mulgcd  12337  mulgcdr  12339  gcddiv  12340  sqgcd  12350  lcmgcdlem  12399  lcmgcd  12400  qredeu  12419  divgcdcoprm0  12423  cncongr1  12425  oddpwdclemdc  12495  sqrt2irraplemnn  12501  qnumdenbi  12514  zgcdsq  12523  hashdvds  12543  phiprmpw  12544  phimullem  12547  eulerthlema  12552  prmdiv  12557  modprm0  12577  coprimeprodsq  12580  pythagtriplem1  12588  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem15  12601  pythagtriplem16  12602  pythagtriplem17  12603  pythagtriplem19  12605  pcval  12619  pcmul  12624  pcdiv  12625  pcqmul  12626  pcid  12647  pcaddlem  12662  pcmpt  12666  pcmpt2  12667  pcmptdvds  12668  pcbc  12674  4sqlem4  12715  mul4sqlem  12716  mul4sq  12717  4sqlem11  12724  4sqlem12  12725  4sqlem15  12728  4sqlem17  12730  ennnfonelemp1  12777  nninfdclemp1  12821  ressvalsets  12896  topnvalg  13083  topnpropgd  13085  prdsex  13101  prdsval  13105  pwsval  13123  qusval  13155  qusex  13157  qusaddvallemg  13165  xpsval  13184  gsumprval  13231  imasmnd2  13284  ismhm  13293  mhmf1o  13302  0mhm  13318  mhmco  13322  mhmeql  13324  gsumfzz  13327  isgrpid2  13372  grpnpcan  13424  imasgrp2  13446  mhmmnd  13452  mulgnndir  13487  mulgdir  13490  isnsg3  13543  isghm  13579  ghmnsgima  13604  ghmf1o  13611  conjghm  13612  qusghm  13618  ablsub4  13649  ghmcmn  13663  invghm  13665  gsumfzmptfidmadd  13675  gsumfzconst  13677  mgpvalg  13685  mgptopng  13691  mgpress  13693  rngdi  13702  rngdir  13703  rngpropd  13717  imasrng  13718  srglmhm  13755  srgrmhm  13756  ringo2times  13790  ringcom  13793  ringpropd  13800  ring1  13821  ringlghm  13823  ringrghm  13824  imasring  13826  opprvalg  13831  opprrng  13839  opprring  13841  invrfvald  13884  dvrvald  13896  dvrdir  13905  rdivmuldivd  13906  islmod  14053  lmodlema  14054  islmodd  14055  lmodcom  14095  lmodnegadd  14098  lmodprop2d  14110  rmodislmod  14113  lsssn0  14132  sraval  14199  qusrhm  14290  gsumfzfsumlemm  14349  expghmap  14369  mulgghm2  14370  mulgrhm  14371  zlmval  14389  znval  14398  psrval  14428  mplvalcoe  14452  cnfval  14666  cnpfval  14667  ispsmet  14795  psmet0  14799  psmettri2  14800  psmetres2  14805  ismet  14816  isxmet  14817  xmettri2  14833  xmetres2  14851  xblss2  14877  xmstri2  14942  mstri2  14943  xmstri  14944  mstri  14945  xmstri3  14946  mstri3  14947  msrtri  14948  comet  14971  bdxmet  14973  txmetcnp  14990  metcnpd  14992  cnmet  15002  ioo2bl  15023  mpomulcn  15038  fsumcncntop  15039  elcncf  15045  mulc1cncf  15061  cncfco  15063  cncfcncntop  15065  cncfmptc  15068  cncfmptid  15069  addccncf  15072  cdivcncfap  15076  negcncf  15077  mulcncflem  15079  limccnp2cntop  15149  reldvg  15151  dvfvalap  15153  eldvap  15154  dvconst  15166  dvconstre  15168  dvconstss  15170  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvexp  15183  dvrecap  15185  dvmptid  15188  dvmptc  15189  dveflem  15198  dvef  15199  elplyd  15213  ply1termlem  15214  plyaddlem1  15219  plymullem1  15220  plyadd  15223  plymul  15224  plycoeid3  15229  plycolemc  15230  plyco  15231  plycjlemc  15232  plycj  15233  plyrecj  15235  dvply1  15237  dvply2g  15238  sinperlem  15280  sinmpi  15287  cosmpi  15288  sinppi  15289  cosppi  15290  efimpi  15291  sinhalfpip  15292  sinhalfpim  15293  coshalfpip  15294  coshalfpim  15295  ptolemy  15296  tangtx  15310  logdivlti  15353  rpcxpadd  15377  rpmulcxp  15381  rplogbchbase  15422  rprelogbmul  15427  binom4  15451  wilthlem1  15452  1sgmprm  15466  1sgm2ppw  15467  sgmmul  15468  mersenne  15469  perfect1  15470  perfectlem2  15472  perfect  15473  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsdilem  15504  lgsdirprm  15511  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  gausslemma2dlem4  15541  gausslemma2dlem6  15544  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad2lem2  15559  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2sqlem2  15592  2sqlem3  15594  2sqlem4  15595  2sqlem8  15600  cvgcmp2nlemabs  15975  trilpolemclim  15979  trilpolemcl  15980  trilpolemisumle  15981  trilpolemeq1  15983  trilpolemlt1  15984  trilpo  15986  redcwlpo  15998  nconstwlpolemgt0  16007  nconstwlpo  16009  neapmkv  16011