Theorem oveq12d 5913

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 5904	. 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 5895

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5898

This theorem is referenced by:  oveq123d  5916  ovmpodxf  6021  ovmpodf  6027  caovdig  6070  caovdir2d  6072  caovdirg  6073  caovdilemd  6087  caovlem2d  6088  offval  6113  ofvalg  6115  offval2  6121  ofco  6124  caofinvl  6128  offres  6159  nnmsucr  6512  nndir  6514  ecovdi  6671  ecovidi  6672  dfplpq2  7382  dfmpq2  7383  addcmpblnq  7395  mulpipqqs  7401  addassnqg  7410  distrnqg  7415  ltaddnq  7435  halfnqq  7438  enq0tr  7462  addcmpblnq0  7471  addnq0mo  7475  addnnnq0  7477  nqnq0a  7482  distrnq0  7487  addassnq0  7490  distnq0r  7491  nq02m  7493  ltexpri  7641  cauappcvgprlemm  7673  cauappcvgprlemloc  7680  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  cauappcvgprlem1  7687  cauappcvgprlem2  7688  cauappcvgprlemlim  7689  cauappcvgpr  7690  caucvgprlemnkj  7694  caucvgprlemnbj  7695  caucvgprlemm  7696  caucvgprlemloc  7703  caucvgprlemcl  7704  caucvgprlemladdfu  7705  caucvgprlemladdrl  7706  caucvgprlem2  7708  caucvgpr  7710  caucvgprprlemelu  7714  caucvgprprlemcbv  7715  caucvgprprlemval  7716  caucvgprprlemmu  7723  caucvgprprlemopu  7727  caucvgprprlemloc  7731  caucvgprprlemclphr  7733  caucvgprprlemexbt  7734  caucvgprprlem2  7738  mulcmpblnrlemg  7768  mulsrmo  7772  mulsrpr  7774  mulcomsrg  7785  distrsrg  7787  recexgt0sr  7801  mulgt0sr  7806  mulextsr1lem  7808  caucvgsrlemgt1  7823  caucvgsr  7830  addcnsr  7862  mulcnsr  7863  recidpirqlemcalc  7885  axaddcl  7892  axmulcl  7894  axmulcom  7899  axmulass  7901  axdistr  7902  axcaucvglemcau  7926  axcaucvglemres  7927  adddir  7977  muladd11  8119  1p1times  8120  muladd11r  8142  pnpcan2  8226  muladd  8370  subdir  8372  mulsub  8387  mulreim  8590  apadd1  8594  mulext1  8598  recextlem1  8637  muleqadd  8654  divdirap  8683  divadddivap  8713  conjmulap  8715  divcanap5rd  8804  subrecap  8825  xp1d2m1eqxm1d2  9200  div4p1lem1div2  9201  cnref1o  9679  xnegid  9888  xposdif  9911  xleaddadd  9916  icoshftf1o  10020  lincmb01cmp  10032  iccf1o  10033  fz01en  10082  fzrev3  10116  fzrevral2  10135  fzrevral3  10136  fzshftral  10137  fzoaddel2  10222  fzosubel  10223  fzosubel2  10224  fzocatel  10228  modqsubdir  10423  addmodlteq  10428  frecuzrdgsuc  10444  frecfzen2  10457  iseqovex  10486  seqvalcd  10489  seq3caopr3  10511  seq3f1olemqsumkj  10528  seq3f1olemqsumk  10529  seq3f1olemqsum  10530  seq3id3  10537  seqfeq3  10542  seq3distr  10543  ser3le  10548  mulexp  10589  mulexpzap  10590  expaddzap  10594  expubnd  10607  subsq  10657  binom2  10662  binom21  10663  binom2sub  10664  binom2sub1  10665  binom3  10668  sqoddm1div8  10704  mulsubdivbinom2ap  10722  nn0opthlem1d  10731  nn0opthd  10733  facp1  10741  facubnd  10756  bcval  10760  bcn1  10769  bcm1k  10771  bcp1n  10772  bcp1nk  10773  bcval5  10774  bcn2  10775  bcpasc  10777  hashun  10816  hashfz  10832  crre  10897  replim  10899  remullem  10911  remul2  10913  immul2  10920  cjcj  10923  cjadd  10924  ipcnval  10926  cjmulval  10928  cjneg  10930  imval2  10934  cjreim  10943  cvg1nlemcau  11024  cvg1nlemres  11025  resqrexlemp1rp  11046  resqrexlemfp1  11049  resqrexlemcalc1  11054  resqrexlemcalc2  11055  resqrex  11066  sqabsadd  11095  sqabssub  11096  absreimsq  11107  recan  11149  amgm2  11158  maxabslemab  11246  maxabslemval  11248  max0addsup  11259  minabs  11275  bdtrilem  11278  bdtri  11279  xrmaxadd  11300  xrminadd  11314  xrbdtri  11315  subcn2  11350  reccn2ap  11352  climle  11373  climcvg1nlem  11388  serf0  11391  fsumadd  11445  fsumsplit  11446  sumpr  11452  sumtp  11453  isumadd  11470  sumsplitdc  11471  fsum2dlemstep  11473  fsumshftm  11484  fisumrev2  11485  fsumconst  11493  modfsummodlemstep  11496  telfsumo  11505  fsumparts  11509  binomlem  11522  binom  11523  binom1dif  11526  bcxmaslem1  11527  isumsplit  11530  isumnn0nn  11532  arisum  11537  arisum2  11538  trireciplem  11539  trirecip  11540  geosergap  11545  geo2sum  11553  geo2sum2  11554  cvgratnnlemsumlt  11567  mertenslemi1  11574  mertensabs  11576  fprodmul  11630  fprodsplitdc  11635  fprodabs  11655  fprod2dlemstep  11661  fproddivapf  11670  eftabs  11695  eftvalcn  11696  efcllemp  11697  ege2le3  11710  efcj  11712  efaddlem  11713  efsep  11730  ef4p  11733  efgt1p2  11734  efgt1p  11735  sinval  11741  cosval  11742  tanvalap  11747  tanval2ap  11752  tanval3ap  11753  efi4p  11756  sinneg  11765  cosneg  11766  tannegap  11767  efival  11771  efmival  11772  sinadd  11775  cosadd  11776  tanaddaplem  11777  tanaddap  11778  sinsub  11779  cossub  11780  addsin  11781  subsin  11782  sinmul  11783  cosmul  11784  addcos  11785  subcos  11786  sincossq  11787  cos2t  11789  sin01bnd  11796  cos01bnd  11797  efieq1re  11810  demoivreALT  11812  dvds2ln  11862  odd2np1lem  11908  gcdaddm  12016  bezoutlemnewy  12028  dfgcd3  12042  dvdsgcd  12044  mulgcd  12048  mulgcdr  12050  gcddiv  12051  sqgcd  12061  lcmgcdlem  12108  lcmgcd  12109  qredeu  12128  divgcdcoprm0  12132  cncongr1  12134  oddpwdclemdc  12204  sqrt2irraplemnn  12210  qnumdenbi  12223  zgcdsq  12232  hashdvds  12252  phiprmpw  12253  phimullem  12256  eulerthlema  12261  prmdiv  12266  modprm0  12285  coprimeprodsq  12288  pythagtriplem1  12296  pythagtriplem12  12306  pythagtriplem14  12308  pythagtriplem15  12309  pythagtriplem16  12310  pythagtriplem17  12311  pythagtriplem19  12313  pcval  12327  pcmul  12332  pcdiv  12333  pcqmul  12334  pcid  12355  pcaddlem  12370  pcmpt  12374  pcmpt2  12375  pcmptdvds  12376  pcbc  12382  4sqlem4  12423  mul4sqlem  12424  mul4sq  12425  4sqlem11  12432  4sqlem12  12433  4sqlem15  12436  4sqlem17  12438  ennnfonelemp1  12456  nninfdclemp1  12500  ressvalsets  12573  topnvalg  12753  topnpropgd  12755  prdsex  12771  qusval  12797  qusex  12799  qusaddvallemg  12806  xpsval  12825  ismhm  12910  mhmf1o  12919  0mhm  12935  mhmco  12939  mhmeql  12941  isgrpid2  12981  grpnpcan  13033  imasgrp2  13049  mhmmnd  13055  mulgnndir  13088  mulgdir  13091  isnsg3  13143  isghm  13179  ghmnsgima  13204  ghmf1o  13211  conjghm  13212  qusghm  13218  ablsub4  13249  ghmcmn  13262  mgpvalg  13274  mgptopng  13280  mgpress  13282  rngdi  13291  rngdir  13292  rngpropd  13306  imasrng  13307  srglmhm  13344  srgrmhm  13345  ringo2times  13379  ringcom  13382  ringpropd  13389  ring1  13408  imasring  13411  opprvalg  13416  opprrng  13424  opprring  13426  invrfvald  13469  dvrvald  13481  dvrdir  13490  rdivmuldivd  13491  islmod  13604  lmodlema  13605  islmodd  13606  lmodcom  13646  lmodnegadd  13649  lmodprop2d  13661  rmodislmod  13664  lsssn0  13683  sraval  13750  mulgghm2  13903  mulgrhm  13904  zlmval  13920  znval  13929  psrval  13941  cnfval  14146  cnpfval  14147  ispsmet  14275  psmet0  14279  psmettri2  14280  psmetres2  14285  ismet  14296  isxmet  14297  xmettri2  14313  xmetres2  14331  xblss2  14357  xmstri2  14422  mstri2  14423  xmstri  14424  mstri  14425  xmstri3  14426  mstri3  14427  msrtri  14428  comet  14451  bdxmet  14453  txmetcnp  14470  metcnpd  14472  cnmet  14482  ioo2bl  14495  fsumcncntop  14508  elcncf  14512  mulc1cncf  14528  cncfco  14530  cncfcncntop  14532  cncfmptc  14534  cncfmptid  14535  addccncf  14538  cdivcncfap  14539  negcncf  14540  mulcncflem  14542  limccnp2cntop  14598  reldvg  14600  dvfvalap  14602  eldvap  14603  dvconst  14613  dvaddxxbr  14617  dvmulxxbr  14618  dvcoapbr  14623  dvcjbr  14624  dvexp  14627  dvrecap  14629  dveflem  14639  dvef  14640  sinperlem  14681  sinmpi  14688  cosmpi  14689  sinppi  14690  cosppi  14691  efimpi  14692  sinhalfpip  14693  sinhalfpim  14694  coshalfpip  14695  coshalfpim  14696  ptolemy  14697  tangtx  14711  logdivlti  14754  rpcxpadd  14778  rpmulcxp  14782  rplogbchbase  14820  rprelogbmul  14825  binom4  14849  wilthlem1  14850  lgsval  14858  lgsfvalg  14859  lgsval2lem  14864  lgsval4a  14876  lgsneg  14878  lgsdilem  14881  lgsdirprm  14888  lgsdir  14889  lgsdilem2  14890  lgsdi  14891  lgsne0  14892  lgseisenlem2  14904  2sqlem2  14915  2sqlem3  14917  2sqlem4  14918  2sqlem8  14923  cvgcmp2nlemabs  15234  trilpolemclim  15238  trilpolemcl  15239  trilpolemisumle  15240  trilpolemeq1  15242  trilpolemlt1  15243  trilpo  15245  redcwlpo  15257  nconstwlpolemgt0  15266  nconstwlpo  15268  neapmkv  15270