Theorem oveq12d 5940

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 5931	. 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 1364  (class class class)co 5922

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  oveq123d  5943  ovmpodxf  6048  ovmpodf  6054  caovdig  6098  caovdir2d  6100  caovdirg  6101  caovdilemd  6115  caovlem2d  6116  offval  6143  ofvalg  6145  offval2  6151  ofco  6154  caofinvl  6160  offres  6192  nnmsucr  6546  nndir  6548  ecovdi  6705  ecovidi  6706  dfplpq2  7421  dfmpq2  7422  addcmpblnq  7434  mulpipqqs  7440  addassnqg  7449  distrnqg  7454  ltaddnq  7474  halfnqq  7477  enq0tr  7501  addcmpblnq0  7510  addnq0mo  7514  addnnnq0  7516  nqnq0a  7521  distrnq0  7526  addassnq0  7529  distnq0r  7530  nq02m  7532  ltexpri  7680  cauappcvgprlemm  7712  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlem2  7727  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemmu  7762  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem2  7777  mulcmpblnrlemg  7807  mulsrmo  7811  mulsrpr  7813  mulcomsrg  7824  distrsrg  7826  recexgt0sr  7840  mulgt0sr  7845  mulextsr1lem  7847  caucvgsrlemgt1  7862  caucvgsr  7869  addcnsr  7901  mulcnsr  7902  recidpirqlemcalc  7924  axaddcl  7931  axmulcl  7933  axmulcom  7938  axmulass  7940  axdistr  7941  axcaucvglemcau  7965  axcaucvglemres  7966  adddir  8017  muladd11  8159  1p1times  8160  muladd11r  8182  pnpcan2  8266  muladd  8410  subdir  8412  mulsub  8427  mulreim  8631  apadd1  8635  mulext1  8639  recextlem1  8678  muleqadd  8695  divdirap  8724  divadddivap  8754  conjmulap  8756  divcanap5rd  8845  subrecap  8866  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  cnref1o  9725  xnegid  9934  xposdif  9957  xleaddadd  9962  icoshftf1o  10066  lincmb01cmp  10078  iccf1o  10079  fz01en  10128  fzrev3  10162  fzrevral2  10181  fzrevral3  10182  fzshftral  10183  fzoaddel2  10269  fzosubel  10270  fzosubel2  10271  fzocatel  10275  modqsubdir  10485  addmodlteq  10490  frecuzrdgsuc  10506  frecfzen2  10519  iseqovex  10550  seqvalcd  10553  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seqf1oglem2  10612  seq3id3  10616  seqfeq3  10621  seq3distr  10624  ser3le  10629  mulexp  10670  mulexpzap  10671  expaddzap  10675  expubnd  10688  subsq  10738  binom2  10743  binom21  10744  binom2sub  10745  binom2sub1  10746  binom3  10749  sqoddm1div8  10785  mulsubdivbinom2ap  10803  nn0opthlem1d  10812  nn0opthd  10814  facp1  10822  facubnd  10837  bcval  10841  bcn1  10850  bcm1k  10852  bcp1n  10853  bcp1nk  10854  bcval5  10855  bcn2  10856  bcpasc  10858  hashun  10897  hashfz  10913  crre  11022  replim  11024  remullem  11036  remul2  11038  immul2  11045  cjcj  11048  cjadd  11049  ipcnval  11051  cjmulval  11053  cjneg  11055  imval2  11059  cjreim  11068  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrex  11191  sqabsadd  11220  sqabssub  11221  absreimsq  11232  recan  11274  amgm2  11283  maxabslemab  11371  maxabslemval  11373  max0addsup  11384  minabs  11401  bdtrilem  11404  bdtri  11405  xrmaxadd  11426  xrminadd  11440  xrbdtri  11441  subcn2  11476  reccn2ap  11478  climle  11499  climcvg1nlem  11514  serf0  11517  fsumadd  11571  fsumsplit  11572  sumpr  11578  sumtp  11579  isumadd  11596  sumsplitdc  11597  fsum2dlemstep  11599  fsumshftm  11610  fisumrev2  11611  fsumconst  11619  modfsummodlemstep  11622  telfsumo  11631  fsumparts  11635  binomlem  11648  binom  11649  binom1dif  11652  bcxmaslem1  11653  isumsplit  11656  isumnn0nn  11658  arisum  11663  arisum2  11664  trireciplem  11665  trirecip  11666  geosergap  11671  geo2sum  11679  geo2sum2  11680  cvgratnnlemsumlt  11693  mertenslemi1  11700  mertensabs  11702  fprodmul  11756  fprodsplitdc  11761  fprodabs  11781  fprod2dlemstep  11787  fproddivapf  11796  eftabs  11821  eftvalcn  11822  efcllemp  11823  ege2le3  11836  efcj  11838  efaddlem  11839  efsep  11856  ef4p  11859  efgt1p2  11860  efgt1p  11861  sinval  11867  cosval  11868  tanvalap  11873  tanval2ap  11878  tanval3ap  11879  efi4p  11882  sinneg  11891  cosneg  11892  tannegap  11893  efival  11897  efmival  11898  sinadd  11901  cosadd  11902  tanaddaplem  11903  tanaddap  11904  sinsub  11905  cossub  11906  addsin  11907  subsin  11908  sinmul  11909  cosmul  11910  addcos  11911  subcos  11912  sincossq  11913  cos2t  11915  sin01bnd  11922  cos01bnd  11923  efieq1re  11937  demoivreALT  11939  dvds2ln  11989  odd2np1lem  12037  gcdaddm  12151  bezoutlemnewy  12163  dfgcd3  12177  dvdsgcd  12179  mulgcd  12183  mulgcdr  12185  gcddiv  12186  sqgcd  12196  lcmgcdlem  12245  lcmgcd  12246  qredeu  12265  divgcdcoprm0  12269  cncongr1  12271  oddpwdclemdc  12341  sqrt2irraplemnn  12347  qnumdenbi  12360  zgcdsq  12369  hashdvds  12389  phiprmpw  12390  phimullem  12393  eulerthlema  12398  prmdiv  12403  modprm0  12423  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  pythagtriplem19  12451  pcval  12465  pcmul  12470  pcdiv  12471  pcqmul  12472  pcid  12493  pcaddlem  12508  pcmpt  12512  pcmpt2  12513  pcmptdvds  12514  pcbc  12520  4sqlem4  12561  mul4sqlem  12562  mul4sq  12563  4sqlem11  12570  4sqlem12  12571  4sqlem15  12574  4sqlem17  12576  ennnfonelemp1  12623  nninfdclemp1  12667  ressvalsets  12742  topnvalg  12922  topnpropgd  12924  prdsex  12940  qusval  12966  qusex  12968  qusaddvallemg  12976  xpsval  12995  gsumprval  13042  ismhm  13093  mhmf1o  13102  0mhm  13118  mhmco  13122  mhmeql  13124  gsumfzz  13127  isgrpid2  13172  grpnpcan  13224  imasgrp2  13240  mhmmnd  13246  mulgnndir  13281  mulgdir  13284  isnsg3  13337  isghm  13373  ghmnsgima  13398  ghmf1o  13405  conjghm  13406  qusghm  13412  ablsub4  13443  ghmcmn  13457  invghm  13459  gsumfzmptfidmadd  13469  gsumfzconst  13471  mgpvalg  13479  mgptopng  13485  mgpress  13487  rngdi  13496  rngdir  13497  rngpropd  13511  imasrng  13512  srglmhm  13549  srgrmhm  13550  ringo2times  13584  ringcom  13587  ringpropd  13594  ring1  13615  ringlghm  13617  ringrghm  13618  imasring  13620  opprvalg  13625  opprrng  13633  opprring  13635  invrfvald  13678  dvrvald  13690  dvrdir  13699  rdivmuldivd  13700  islmod  13847  lmodlema  13848  islmodd  13849  lmodcom  13889  lmodnegadd  13892  lmodprop2d  13904  rmodislmod  13907  lsssn0  13926  sraval  13993  qusrhm  14084  gsumfzfsumlemm  14143  expghmap  14163  mulgghm2  14164  mulgrhm  14165  zlmval  14183  znval  14192  psrval  14220  cnfval  14430  cnpfval  14431  ispsmet  14559  psmet0  14563  psmettri2  14564  psmetres2  14569  ismet  14580  isxmet  14581  xmettri2  14597  xmetres2  14615  xblss2  14641  xmstri2  14706  mstri2  14707  xmstri  14708  mstri  14709  xmstri3  14710  mstri3  14711  msrtri  14712  comet  14735  bdxmet  14737  txmetcnp  14754  metcnpd  14756  cnmet  14766  ioo2bl  14787  mpomulcn  14802  fsumcncntop  14803  elcncf  14809  mulc1cncf  14825  cncfco  14827  cncfcncntop  14829  cncfmptc  14832  cncfmptid  14833  addccncf  14836  cdivcncfap  14840  negcncf  14841  mulcncflem  14843  limccnp2cntop  14913  reldvg  14915  dvfvalap  14917  eldvap  14918  dvconst  14930  dvconstre  14932  dvconstss  14934  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvexp  14947  dvrecap  14949  dvmptid  14952  dvmptc  14953  dveflem  14962  dvef  14963  elplyd  14977  ply1termlem  14978  plyaddlem1  14983  plymullem1  14984  plyadd  14987  plymul  14988  plycoeid3  14993  plycolemc  14994  plyco  14995  plycjlemc  14996  plycj  14997  plyrecj  14999  dvply1  15001  dvply2g  15002  sinperlem  15044  sinmpi  15051  cosmpi  15052  sinppi  15053  cosppi  15054  efimpi  15055  sinhalfpip  15056  sinhalfpim  15057  coshalfpip  15058  coshalfpim  15059  ptolemy  15060  tangtx  15074  logdivlti  15117  rpcxpadd  15141  rpmulcxp  15145  rplogbchbase  15186  rprelogbmul  15191  binom4  15215  wilthlem1  15216  1sgmprm  15230  1sgm2ppw  15231  sgmmul  15232  mersenne  15233  perfect1  15234  perfectlem2  15236  perfect  15237  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsval4a  15263  lgsneg  15265  lgsdilem  15268  lgsdirprm  15275  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  gausslemma2dlem4  15305  gausslemma2dlem6  15308  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad2lem2  15323  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2sqlem2  15356  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  cvgcmp2nlemabs  15676  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trilpo  15687  redcwlpo  15699  nconstwlpolemgt0  15708  nconstwlpo  15710  neapmkv  15712