Theorem oveq12d 6070

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 6061	. 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 1398  (class class class)co 6052

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  oveq123d  6073  ovmpodxf  6181  ovmpodf  6187  caovdig  6231  caovdir2d  6233  caovdirg  6234  caovdilemd  6248  caovlem2d  6249  offval  6276  ofvalg  6278  offval2  6284  ofco  6287  caofinvl  6294  offres  6330  nnmsucr  6723  nndir  6725  ecovdi  6882  ecovidi  6883  dfplpq2  7671  dfmpq2  7672  addcmpblnq  7684  mulpipqqs  7690  addassnqg  7699  distrnqg  7704  ltaddnq  7724  halfnqq  7727  enq0tr  7751  addcmpblnq0  7760  addnq0mo  7764  addnnnq0  7766  nqnq0a  7771  distrnq0  7776  addassnq0  7779  distnq0r  7780  nq02m  7782  ltexpri  7930  cauappcvgprlemm  7962  cauappcvgprlemloc  7969  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlem2  7977  cauappcvgprlemlim  7978  cauappcvgpr  7979  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemloc  7992  caucvgprlemcl  7993  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem2  7997  caucvgpr  7999  caucvgprprlemelu  8003  caucvgprprlemcbv  8004  caucvgprprlemval  8005  caucvgprprlemmu  8012  caucvgprprlemopu  8016  caucvgprprlemloc  8020  caucvgprprlemclphr  8022  caucvgprprlemexbt  8023  caucvgprprlem2  8027  mulcmpblnrlemg  8057  mulsrmo  8061  mulsrpr  8063  mulcomsrg  8074  distrsrg  8076  recexgt0sr  8090  mulgt0sr  8095  mulextsr1lem  8097  caucvgsrlemgt1  8112  caucvgsr  8119  addcnsr  8151  mulcnsr  8152  recidpirqlemcalc  8174  axaddcl  8181  axmulcl  8183  axmulcom  8188  axmulass  8190  axdistr  8191  axcaucvglemcau  8215  axcaucvglemres  8216  adddir  8267  muladd11  8408  1p1times  8409  muladd11r  8431  pnpcan2  8515  muladd  8659  subdir  8661  mulsub  8676  mulreim  8880  apadd1  8884  mulext1  8888  recextlem1  8927  muleqadd  8944  divdirap  8973  divadddivap  9003  conjmulap  9005  divcanap5rd  9094  subrecap  9115  xp1d2m1eqxm1d2  9493  div4p1lem1div2  9494  cnref1o  9986  xnegid  10195  xposdif  10218  xleaddadd  10223  icoshftf1o  10327  lincmb01cmp  10339  iccf1o  10341  fz01en  10390  fzrev3  10425  fzrevral2  10444  fzrevral3  10445  fzshftral  10446  fzoaddel2  10539  fzosubel  10543  fzosubel2  10544  fzocatel  10548  modqsubdir  10759  addmodlteq  10764  frecuzrdgsuc  10780  frecfzen2  10793  iseqovex  10824  seqvalcd  10827  seq3caopr3  10857  seqcaopr3g  10858  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seqf1oglem2  10886  seq3id3  10890  seqfeq3  10895  seq3distr  10898  ser3le  10903  mulexp  10944  mulexpzap  10945  expaddzap  10949  expubnd  10962  subsq  11012  binom2  11017  binom21  11018  binom2sub  11019  binom2sub1  11020  binom3  11023  sqoddm1div8  11059  mulsubdivbinom2ap  11077  nn0opthlem1d  11086  nn0opthd  11088  facp1  11096  facubnd  11111  bcval  11115  bcn1  11124  bcm1k  11126  bcp1n  11127  bcp1nk  11128  bcval5  11129  bcn2  11130  bcpasc  11132  bcm1n  11135  hashun  11173  hashfz  11190  hashfibclem  11210  hashfibc  11211  hashtpgim  11221  ccatlid  11298  ccatass  11300  ccat1st1st  11333  swrdval  11344  swrdspsleq  11363  ccatswrd  11366  pfxval  11370  addlenpfx  11387  ccatpfx  11397  ccatopth  11412  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12  11429  swrdccat  11431  swrdccat3blem  11435  swrdccatin2d  11440  pfxccatin12d  11441  cats1lend  11463  cats2catd  11465  s2eqd  11466  s3eqd  11467  s4eqd  11468  s5eqd  11469  s6eqd  11470  s7eqd  11471  s8eqd  11472  crre  11546  replim  11548  remullem  11560  remul2  11562  immul2  11569  cjcj  11572  cjadd  11573  ipcnval  11575  cjmulval  11577  cjneg  11579  imval2  11583  cjreim  11592  cvg1nlemcau  11673  cvg1nlemres  11674  resqrexlemp1rp  11695  resqrexlemfp1  11698  resqrexlemcalc1  11703  resqrexlemcalc2  11704  resqrex  11715  sqabsadd  11744  sqabssub  11745  absreimsq  11756  recan  11798  amgm2  11807  maxabslemab  11895  maxabslemval  11897  max0addsup  11908  minabs  11925  bdtrilem  11928  bdtri  11929  xrmaxadd  11950  xrminadd  11964  xrbdtri  11965  subcn2  12000  reccn2ap  12002  climle  12023  climcvg1nlem  12038  serf0  12041  fsumadd  12096  fsumsplit  12097  sumpr  12103  sumtp  12104  isumadd  12121  sumsplitdc  12122  fsum2dlemstep  12124  fsumshftm  12135  fisumrev2  12136  fsumconst  12144  modfsummodlemstep  12147  telfsumo  12156  fsumparts  12160  binomlem  12173  binom  12174  binom1dif  12177  bcxmaslem1  12178  isumsplit  12181  isumnn0nn  12183  arisum  12188  arisum2  12189  trireciplem  12190  trirecip  12191  geosergap  12196  geo2sum  12204  geo2sum2  12205  cvgratnnlemsumlt  12218  mertenslemi1  12225  mertensabs  12227  fprodmul  12281  fprodsplitdc  12286  fprodabs  12306  fprod2dlemstep  12312  fproddivapf  12321  eftabs  12346  eftvalcn  12347  efcllemp  12348  ege2le3  12361  efcj  12363  efaddlem  12364  efsep  12381  ef4p  12384  efgt1p2  12385  efgt1p  12386  sinval  12392  cosval  12393  tanvalap  12398  tanval2ap  12403  tanval3ap  12404  efi4p  12407  sinneg  12416  cosneg  12417  tannegap  12418  efival  12422  efmival  12423  sinadd  12426  cosadd  12427  tanaddaplem  12428  tanaddap  12429  sinsub  12430  cossub  12431  addsin  12432  subsin  12433  sinmul  12434  cosmul  12435  addcos  12436  subcos  12437  sincossq  12438  cos2t  12440  sin01bnd  12447  cos01bnd  12448  efieq1re  12462  demoivreALT  12464  dvds2ln  12514  odd2np1lem  12562  bitsinv1lem  12651  gcdaddm  12684  bezoutlemnewy  12696  dfgcd3  12710  dvdsgcd  12712  mulgcd  12716  mulgcdr  12718  gcddiv  12719  sqgcd  12729  lcmgcdlem  12778  lcmgcd  12779  qredeu  12798  divgcdcoprm0  12802  cncongr1  12804  oddpwdclemdc  12874  sqrt2irraplemnn  12880  qnumdenbi  12893  zgcdsq  12902  hashdvds  12922  phiprmpw  12923  phimullem  12926  eulerthlema  12931  prmdiv  12936  modprm0  12956  coprimeprodsq  12959  pythagtriplem1  12967  pythagtriplem12  12977  pythagtriplem14  12979  pythagtriplem15  12980  pythagtriplem16  12981  pythagtriplem17  12982  pythagtriplem19  12984  pcval  12998  pcmul  13003  pcdiv  13004  pcqmul  13005  pcid  13026  pcaddlem  13041  pcmpt  13045  pcmpt2  13046  pcmptdvds  13047  pcbc  13053  4sqlem4  13094  mul4sqlem  13095  mul4sq  13096  4sqlem11  13103  4sqlem12  13104  4sqlem15  13107  4sqlem17  13109  ballotfilemfval  13150  ballotfilemfp1  13152  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemfmpn  13155  ennnfonelemp1  13174  nninfdclemp1  13218  ressvalsets  13294  topnvalg  13481  topnpropgd  13483  prdsex  13499  prdsval  13503  pwsval  13521  qusval  13553  qusex  13555  qusaddvallemg  13563  xpsval  13582  gsumprval  13629  imasmnd2  13682  ismhm  13691  mhmf1o  13700  0mhm  13716  mhmco  13720  mhmeql  13722  gsumfzz  13725  isgrpid2  13770  grpnpcan  13822  imasgrp2  13844  mhmmnd  13850  mulgnndir  13885  mulgdir  13888  isnsg3  13941  isghm  13977  ghmnsgima  14002  ghmf1o  14009  conjghm  14010  qusghm  14016  ablsub4  14047  ghmcmn  14061  invghm  14063  gsumfzmptfidmadd  14073  gsumfzconst  14075  mgpvalg  14084  mgptopng  14090  mgpress  14092  rngdi  14101  rngdir  14102  rngpropd  14116  imasrng  14117  srglmhm  14154  srgrmhm  14155  ringo2times  14189  ringcom  14192  ringpropd  14199  ring1  14220  ringlghm  14222  ringrghm  14223  imasring  14225  opprvalg  14230  opprrng  14238  opprring  14240  invrfvald  14284  dvrvald  14296  dvrdir  14305  rdivmuldivd  14306  islmod  14456  lmodlema  14457  islmodd  14458  lmodcom  14498  lmodnegadd  14501  lmodprop2d  14513  rmodislmod  14516  lsssn0  14535  sraval  14602  qusrhm  14693  gsumfzfsumlemm  14752  expghmap  14772  mulgghm2  14773  mulgrhm  14774  zlmval  14792  znval  14801  psrval  14831  mplvalcoe  14862  cnfval  15076  cnpfval  15077  ispsmet  15205  psmet0  15209  psmettri2  15210  psmetres2  15215  ismet  15226  isxmet  15227  xmettri2  15243  xmetres2  15261  xblss2  15287  xmstri2  15352  mstri2  15353  xmstri  15354  mstri  15355  xmstri3  15356  mstri3  15357  msrtri  15358  comet  15381  bdxmet  15383  txmetcnp  15400  metcnpd  15402  cnmet  15412  ioo2bl  15433  mpomulcn  15448  fsumcncntop  15449  elcncf  15455  mulc1cncf  15471  cncfco  15473  cncfcncntop  15475  cncfmptc  15478  cncfmptid  15479  addccncf  15482  cdivcncfap  15486  negcncf  15487  mulcncflem  15489  limccnp2cntop  15559  reldvg  15561  dvfvalap  15563  eldvap  15564  dvconst  15576  dvconstre  15578  dvconstss  15580  dvaddxxbr  15583  dvmulxxbr  15584  dvcoapbr  15589  dvcjbr  15590  dvexp  15593  dvrecap  15595  dvmptid  15598  dvmptc  15599  dveflem  15608  dvef  15609  elplyd  15623  ply1termlem  15624  plyaddlem1  15629  plymullem1  15630  plyadd  15633  plymul  15634  plycoeid3  15639  plycolemc  15640  plyco  15641  plycjlemc  15642  plycj  15643  plyrecj  15645  dvply1  15647  dvply2g  15648  sinperlem  15690  sinmpi  15697  cosmpi  15698  sinppi  15699  cosppi  15700  efimpi  15701  sinhalfpip  15702  sinhalfpim  15703  coshalfpip  15704  coshalfpim  15705  ptolemy  15706  tangtx  15720  logdivlti  15763  rpcxpadd  15787  rpmulcxp  15791  rplogbchbase  15832  rprelogbmul  15837  binom4  15861  pellexlem2  15863  pellexlem3  15864  wilthlem1  15865  1sgmprm  15879  1sgm2ppw  15880  sgmmul  15881  mersenne  15882  perfect1  15883  perfectlem2  15885  perfect  15886  lgsval  15894  lgsfvalg  15895  lgsval2lem  15900  lgsval4a  15912  lgsneg  15914  lgsdilem  15917  lgsdirprm  15924  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  gausslemma2dlem4  15954  gausslemma2dlem6  15957  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  lgsquad2lem1  15971  lgsquad2lem2  15972  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2sqlem2  16005  2sqlem3  16007  2sqlem4  16008  2sqlem8  16013  vtxdgfval  16300  vtxdgfifival  16303  vtxdgop  16304  vtxdgfi0e  16307  vtxdeqd  16308  vtxdfifiun  16309  vtxduspgrfvedgfi  16313  1loopgrvd2fi  16317  repiecele0  16827  repiecege0  16828  repiecef  16829  cvgcmp2nlemabs  16833  trilpolemclim  16837  trilpolemcl  16838  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  trilpo  16844  redcwlpo  16857  nconstwlpolemgt0  16867  nconstwlpo  16869  neapmkv  16871  gsumgfsum  16883  gfsump1  16885  gfsumz  16886