Theorem oveq12d 5964

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 5955	. 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 5946

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 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  oveq123d  5967  ovmpodxf  6073  ovmpodf  6079  caovdig  6123  caovdir2d  6125  caovdirg  6126  caovdilemd  6140  caovlem2d  6141  offval  6168  ofvalg  6170  offval2  6176  ofco  6179  caofinvl  6186  offres  6222  nnmsucr  6576  nndir  6578  ecovdi  6735  ecovidi  6736  dfplpq2  7469  dfmpq2  7470  addcmpblnq  7482  mulpipqqs  7488  addassnqg  7497  distrnqg  7502  ltaddnq  7522  halfnqq  7525  enq0tr  7549  addcmpblnq0  7558  addnq0mo  7562  addnnnq0  7564  nqnq0a  7569  distrnq0  7574  addassnq0  7577  distnq0r  7578  nq02m  7580  ltexpri  7728  cauappcvgprlemm  7760  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlem2  7775  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemloc  7790  caucvgprlemcl  7791  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemmu  7810  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlemclphr  7820  caucvgprprlemexbt  7821  caucvgprprlem2  7825  mulcmpblnrlemg  7855  mulsrmo  7859  mulsrpr  7861  mulcomsrg  7872  distrsrg  7874  recexgt0sr  7888  mulgt0sr  7893  mulextsr1lem  7895  caucvgsrlemgt1  7910  caucvgsr  7917  addcnsr  7949  mulcnsr  7950  recidpirqlemcalc  7972  axaddcl  7979  axmulcl  7981  axmulcom  7986  axmulass  7988  axdistr  7989  axcaucvglemcau  8013  axcaucvglemres  8014  adddir  8065  muladd11  8207  1p1times  8208  muladd11r  8230  pnpcan2  8314  muladd  8458  subdir  8460  mulsub  8475  mulreim  8679  apadd1  8683  mulext1  8687  recextlem1  8726  muleqadd  8743  divdirap  8772  divadddivap  8802  conjmulap  8804  divcanap5rd  8893  subrecap  8914  xp1d2m1eqxm1d2  9292  div4p1lem1div2  9293  cnref1o  9774  xnegid  9983  xposdif  10006  xleaddadd  10011  icoshftf1o  10115  lincmb01cmp  10127  iccf1o  10128  fz01en  10177  fzrev3  10211  fzrevral2  10230  fzrevral3  10231  fzshftral  10232  fzoaddel2  10321  fzosubel  10325  fzosubel2  10326  fzocatel  10330  modqsubdir  10540  addmodlteq  10545  frecuzrdgsuc  10561  frecfzen2  10574  iseqovex  10605  seqvalcd  10608  seq3caopr3  10638  seqcaopr3g  10639  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seqf1oglem2  10667  seq3id3  10671  seqfeq3  10676  seq3distr  10679  ser3le  10684  mulexp  10725  mulexpzap  10726  expaddzap  10730  expubnd  10743  subsq  10793  binom2  10798  binom21  10799  binom2sub  10800  binom2sub1  10801  binom3  10804  sqoddm1div8  10840  mulsubdivbinom2ap  10858  nn0opthlem1d  10867  nn0opthd  10869  facp1  10877  facubnd  10892  bcval  10896  bcn1  10905  bcm1k  10907  bcp1n  10908  bcp1nk  10909  bcval5  10910  bcn2  10911  bcpasc  10913  hashun  10952  hashfz  10968  ccatlid  11065  ccatass  11067  ccat1st1st  11096  swrdval  11104  swrdspsleq  11123  ccatswrd  11126  pfxval  11130  addlenpfx  11145  ccatpfx  11155  crre  11201  replim  11203  remullem  11215  remul2  11217  immul2  11224  cjcj  11227  cjadd  11228  ipcnval  11230  cjmulval  11232  cjneg  11234  imval2  11238  cjreim  11247  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemp1rp  11350  resqrexlemfp1  11353  resqrexlemcalc1  11358  resqrexlemcalc2  11359  resqrex  11370  sqabsadd  11399  sqabssub  11400  absreimsq  11411  recan  11453  amgm2  11462  maxabslemab  11550  maxabslemval  11552  max0addsup  11563  minabs  11580  bdtrilem  11583  bdtri  11584  xrmaxadd  11605  xrminadd  11619  xrbdtri  11620  subcn2  11655  reccn2ap  11657  climle  11678  climcvg1nlem  11693  serf0  11696  fsumadd  11750  fsumsplit  11751  sumpr  11757  sumtp  11758  isumadd  11775  sumsplitdc  11776  fsum2dlemstep  11778  fsumshftm  11789  fisumrev2  11790  fsumconst  11798  modfsummodlemstep  11801  telfsumo  11810  fsumparts  11814  binomlem  11827  binom  11828  binom1dif  11831  bcxmaslem1  11832  isumsplit  11835  isumnn0nn  11837  arisum  11842  arisum2  11843  trireciplem  11844  trirecip  11845  geosergap  11850  geo2sum  11858  geo2sum2  11859  cvgratnnlemsumlt  11872  mertenslemi1  11879  mertensabs  11881  fprodmul  11935  fprodsplitdc  11940  fprodabs  11960  fprod2dlemstep  11966  fproddivapf  11975  eftabs  12000  eftvalcn  12001  efcllemp  12002  ege2le3  12015  efcj  12017  efaddlem  12018  efsep  12035  ef4p  12038  efgt1p2  12039  efgt1p  12040  sinval  12046  cosval  12047  tanvalap  12052  tanval2ap  12057  tanval3ap  12058  efi4p  12061  sinneg  12070  cosneg  12071  tannegap  12072  efival  12076  efmival  12077  sinadd  12080  cosadd  12081  tanaddaplem  12082  tanaddap  12083  sinsub  12084  cossub  12085  addsin  12086  subsin  12087  sinmul  12088  cosmul  12089  addcos  12090  subcos  12091  sincossq  12092  cos2t  12094  sin01bnd  12101  cos01bnd  12102  efieq1re  12116  demoivreALT  12118  dvds2ln  12168  odd2np1lem  12216  bitsinv1lem  12305  gcdaddm  12338  bezoutlemnewy  12350  dfgcd3  12364  dvdsgcd  12366  mulgcd  12370  mulgcdr  12372  gcddiv  12373  sqgcd  12383  lcmgcdlem  12432  lcmgcd  12433  qredeu  12452  divgcdcoprm0  12456  cncongr1  12458  oddpwdclemdc  12528  sqrt2irraplemnn  12534  qnumdenbi  12547  zgcdsq  12556  hashdvds  12576  phiprmpw  12577  phimullem  12580  eulerthlema  12585  prmdiv  12590  modprm0  12610  coprimeprodsq  12613  pythagtriplem1  12621  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem15  12634  pythagtriplem16  12635  pythagtriplem17  12636  pythagtriplem19  12638  pcval  12652  pcmul  12657  pcdiv  12658  pcqmul  12659  pcid  12680  pcaddlem  12695  pcmpt  12699  pcmpt2  12700  pcmptdvds  12701  pcbc  12707  4sqlem4  12748  mul4sqlem  12749  mul4sq  12750  4sqlem11  12757  4sqlem12  12758  4sqlem15  12761  4sqlem17  12763  ennnfonelemp1  12810  nninfdclemp1  12854  ressvalsets  12929  topnvalg  13116  topnpropgd  13118  prdsex  13134  prdsval  13138  pwsval  13156  qusval  13188  qusex  13190  qusaddvallemg  13198  xpsval  13217  gsumprval  13264  imasmnd2  13317  ismhm  13326  mhmf1o  13335  0mhm  13351  mhmco  13355  mhmeql  13357  gsumfzz  13360  isgrpid2  13405  grpnpcan  13457  imasgrp2  13479  mhmmnd  13485  mulgnndir  13520  mulgdir  13523  isnsg3  13576  isghm  13612  ghmnsgima  13637  ghmf1o  13644  conjghm  13645  qusghm  13651  ablsub4  13682  ghmcmn  13696  invghm  13698  gsumfzmptfidmadd  13708  gsumfzconst  13710  mgpvalg  13718  mgptopng  13724  mgpress  13726  rngdi  13735  rngdir  13736  rngpropd  13750  imasrng  13751  srglmhm  13788  srgrmhm  13789  ringo2times  13823  ringcom  13826  ringpropd  13833  ring1  13854  ringlghm  13856  ringrghm  13857  imasring  13859  opprvalg  13864  opprrng  13872  opprring  13874  invrfvald  13917  dvrvald  13929  dvrdir  13938  rdivmuldivd  13939  islmod  14086  lmodlema  14087  islmodd  14088  lmodcom  14128  lmodnegadd  14131  lmodprop2d  14143  rmodislmod  14146  lsssn0  14165  sraval  14232  qusrhm  14323  gsumfzfsumlemm  14382  expghmap  14402  mulgghm2  14403  mulgrhm  14404  zlmval  14422  znval  14431  psrval  14461  mplvalcoe  14485  cnfval  14699  cnpfval  14700  ispsmet  14828  psmet0  14832  psmettri2  14833  psmetres2  14838  ismet  14849  isxmet  14850  xmettri2  14866  xmetres2  14884  xblss2  14910  xmstri2  14975  mstri2  14976  xmstri  14977  mstri  14978  xmstri3  14979  mstri3  14980  msrtri  14981  comet  15004  bdxmet  15006  txmetcnp  15023  metcnpd  15025  cnmet  15035  ioo2bl  15056  mpomulcn  15071  fsumcncntop  15072  elcncf  15078  mulc1cncf  15094  cncfco  15096  cncfcncntop  15098  cncfmptc  15101  cncfmptid  15102  addccncf  15105  cdivcncfap  15109  negcncf  15110  mulcncflem  15112  limccnp2cntop  15182  reldvg  15184  dvfvalap  15186  eldvap  15187  dvconst  15199  dvconstre  15201  dvconstss  15203  dvaddxxbr  15206  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvexp  15216  dvrecap  15218  dvmptid  15221  dvmptc  15222  dveflem  15231  dvef  15232  elplyd  15246  ply1termlem  15247  plyaddlem1  15252  plymullem1  15253  plyadd  15256  plymul  15257  plycoeid3  15262  plycolemc  15263  plyco  15264  plycjlemc  15265  plycj  15266  plyrecj  15268  dvply1  15270  dvply2g  15271  sinperlem  15313  sinmpi  15320  cosmpi  15321  sinppi  15322  cosppi  15323  efimpi  15324  sinhalfpip  15325  sinhalfpim  15326  coshalfpip  15327  coshalfpim  15328  ptolemy  15329  tangtx  15343  logdivlti  15386  rpcxpadd  15410  rpmulcxp  15414  rplogbchbase  15455  rprelogbmul  15460  binom4  15484  wilthlem1  15485  1sgmprm  15499  1sgm2ppw  15500  sgmmul  15501  mersenne  15502  perfect1  15503  perfectlem2  15505  perfect  15506  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsval4a  15532  lgsneg  15534  lgsdilem  15537  lgsdirprm  15544  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  gausslemma2dlem4  15574  gausslemma2dlem6  15577  lgseisenlem2  15581  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  lgsquad2lem2  15592  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2sqlem2  15625  2sqlem3  15627  2sqlem4  15628  2sqlem8  15633  cvgcmp2nlemabs  16008  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trilpo  16019  redcwlpo  16031  nconstwlpolemgt0  16040  nconstwlpo  16042  neapmkv  16044