Theorem oveq12d 6106

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 6097	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A F C ) = ( B F D ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402  (class class class)co 6088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq123d  6109  ovmpodxf  6217  ovmpodf  6223  caovdig  6267  caovdir2d  6269  caovdirg  6270  caovdilemd  6284  caovlem2d  6285  offval  6314  ofvalg  6316  offval2  6322  ofco  6325  caofinvl  6332  offres  6372  nnmsucr  6765  nndir  6767  ecovdi  6924  ecovidi  6925  dfplpq2  7727  dfmpq2  7728  addcmpblnq  7740  mulpipqqs  7746  addassnqg  7755  distrnqg  7760  ltaddnq  7780  halfnqq  7783  enq0tr  7807  addcmpblnq0  7816  addnq0mo  7820  addnnnq0  7822  nqnq0a  7827  distrnq0  7832  addassnq0  7835  distnq0r  7836  nq02m  7838  ltexpri  7986  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemmu  8068  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlem2  8083  mulcmpblnrlemg  8113  mulsrmo  8117  mulsrpr  8119  mulcomsrg  8130  distrsrg  8132  recexgt0sr  8146  mulgt0sr  8151  mulextsr1lem  8153  caucvgsrlemgt1  8168  caucvgsr  8175  addcnsr  8207  mulcnsr  8208  recidpirqlemcalc  8230  axaddcl  8237  axmulcl  8239  axmulcom  8244  axmulass  8246  axdistr  8247  axcaucvglemcau  8271  axcaucvglemres  8272  adddir  8323  muladd11  8466  1p1times  8467  muladd11r  8489  pnpcan2  8573  muladd  8718  subdir  8720  mulsub  8735  mulreim  8940  apadd1  8944  mulext1  8948  recextlem1  8987  muleqadd  9006  divdirap  9035  divadddivap  9065  conjmulap  9067  divcanap5rd  9156  subrecap  9177  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  cnref1o  10068  xnegid  10278  xposdif  10301  xleaddadd  10306  icoshftf1o  10410  lincmb01cmp  10422  iccf1o  10424  fz01en  10476  fzrev3  10511  fzrevral2  10530  fzrevral3  10531  fzshftral  10532  fzoaddel2  10625  fzosubel  10629  fzosubel2  10630  fzocatel  10634  modqsubdir  10851  addmodlteq  10856  frecuzrdgsuc  10872  frecfzen2  10885  iseqovex  10916  seqvalcd  10919  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seqf1oglem2  10978  seq3id3  10982  seqfeq3  10987  seq3distr  10990  ser3le  10995  mulexp  11036  mulexpzap  11037  expaddzap  11041  expubnd  11054  subsq  11104  binom2  11109  binom21  11110  binom2sub  11111  binom2sub1  11112  binom3  11115  sqoddm1div8  11152  mulsubdivbinom2ap  11171  nn0opthlem1d  11180  nn0opthd  11182  facp1  11190  facubnd  11205  bcval  11209  bcn1  11218  bcm1k  11220  bcp1n  11221  bcp1nk  11222  bcval5  11223  bcn2  11224  bcpasc  11226  bcm1n  11229  hashun  11267  hashfz  11284  hashfibclem  11304  hashfibc  11305  hashf1lem2  11308  hashf1  11309  hashtpgim  11319  ccatlid  11396  ccatass  11398  ccat1st1st  11431  swrdval  11442  swrdspsleq  11461  ccatswrd  11464  pfxval  11468  addlenpfx  11485  ccatpfx  11495  ccatopth  11510  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat  11529  swrdccat3blem  11533  swrdccatin2d  11538  pfxccatin12d  11539  cats1lend  11561  cats2catd  11563  s2eqd  11564  s3eqd  11565  s4eqd  11566  s5eqd  11567  s6eqd  11568  s7eqd  11569  s8eqd  11570  crre  11644  replim  11646  remullem  11658  remul2  11660  immul2  11667  cjcj  11670  cjadd  11671  ipcnval  11673  cjmulval  11675  cjneg  11677  imval2  11681  cjreim  11691  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrex  11814  sqabsadd  11843  sqabssub  11844  absreimsq  11855  recan  11898  amgm2  11907  maxabslemab  11995  maxabslemval  11997  max0addsup  12008  minabs  12026  bdtrilem  12030  bdtri  12031  xrmaxadd  12052  xrminadd  12066  xrbdtri  12067  subcn2  12102  reccn2ap  12104  climle  12125  climcvg1nlem  12140  serf0  12143  fsumadd  12198  fsumsplit  12199  sumpr  12205  sumtp  12206  isumadd  12223  sumsplitdc  12224  fsum2dlemstep  12226  fsumshftm  12237  fisumrev2  12238  fsumconst  12246  modfsummodlemstep  12249  telfsumo  12258  fsumparts  12262  binomlem  12275  binom  12276  binom1dif  12279  bcxmaslem1  12280  isumsplit  12283  isumnn0nn  12285  arisum  12290  arisum2  12291  trireciplem  12292  trirecip  12293  geosergap  12298  geo2sum  12306  geo2sum2  12307  cvgratnnlemsumlt  12320  mertenslemi1  12327  mertensabs  12329  fprodmul  12383  fprodsplitdc  12388  fprodabs  12408  fprod2dlemstep  12414  fproddivapf  12423  eftabs  12448  eftvalcn  12449  efcllemp  12450  ege2le3  12463  efcj  12465  efaddlem  12466  efsep  12483  ef4p  12486  efgt1p2  12487  efgt1p  12488  sinval  12494  cosval  12495  tanvalap  12500  tanval2ap  12505  tanval3ap  12506  efi4p  12509  sinneg  12518  cosneg  12519  tannegap  12520  efival  12524  efmival  12525  sinadd  12528  cosadd  12529  tanaddaplem  12530  tanaddap  12531  sinsub  12532  cossub  12533  addsin  12534  subsin  12535  sinmul  12536  cosmul  12537  addcos  12538  subcos  12539  sincossq  12540  cos2t  12542  sin01bnd  12549  cos01bnd  12550  efieq1re  12564  demoivreALT  12566  dvds2ln  12616  odd2np1lem  12664  bitsinv1lem  12753  gcdaddm  12786  bezoutlemnewy  12798  dfgcd3  12812  dvdsgcd  12814  mulgcd  12818  mulgcdr  12820  gcddiv  12821  sqgcd  12831  lcmgcdlem  12880  lcmgcd  12881  qredeu  12900  divgcdcoprm0  12904  cncongr1  12906  nnmaxpwlemparts  12977  sqrt2irraplemnn  12984  qnumdenbi  12997  zgcdsq  13006  hashdvds  13028  phiprmpw  13029  phimullem  13032  eulerthlema  13037  prmdiv  13042  modprm0  13062  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem19  13090  pcval  13104  pcmul  13109  pcdiv  13110  pcqmul  13111  pcid  13132  pcaddlem  13147  pcmpt  13151  pcmpt2  13152  pcmptdvds  13153  pcbc  13159  4sqlem4  13200  mul4sqlem  13201  mul4sq  13202  4sqlem11  13209  4sqlem12  13210  4sqlem15  13213  4sqlem17  13215  ballotfilemfval  13287  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemgval  13325  ballotfilemgun  13326  ballotfilemfrc  13328  ballotfilemfrceq  13330  ennnfonelemp1  13355  nninfdclemp1  13399  ressvalsets  13476  topnvalg  13664  topnpropgd  13666  qusval  13703  qusex  13705  qusaddvallemg  13713  imasmnd2  13818  ismhm  13827  mhmf1o  13836  0mhm  13852  mhmco  13856  mhmeql  13858  isgrpid2  13904  grpnpcan  13956  imasgrp2  13972  mhmmnd  13978  mulgnndir  14013  mulgdir  14016  isnsg3  14069  isghm  14105  ghmnsgima  14130  ghmf1o  14137  conjghm  14138  qusghm  14144  ablsub4  14207  ghmcmn  14221  invghm  14223  gzsumconst  14233  gzsumgsum  14245  gsump1  14247  gsumzfi  14248  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsummptfidmsplitres  14255  gsumsplitfi  14256  gsumsnfdcmn  14257  gsumconstcmn  14266  prdsex  14279  prdsval  14280  xpsval  14308  pwsval  14311  mgpvalg  14327  mgptopng  14335  mgpress  14337  rngdi  14346  rngdir  14347  rngpropd  14361  imasrng  14362  srglmhm  14404  srgrmhm  14405  ringo2times  14440  ringcom  14443  ringpropd  14450  ring1  14471  ringlghm  14473  ringrghm  14474  imasring  14478  opprvalg  14483  opprrng  14491  opprring  14493  invrfvald  14538  dvrvald  14550  dvrdir  14559  rdivmuldivd  14560  islmod  14736  lmodlema  14737  islmodd  14738  lmodcom  14779  lmodnegadd  14782  lmodprop2d  14794  rmodislmod  14797  lsssn0  14816  sraval  14883  qusrhm  14974  gsumfsum  15032  expghmap  15051  mulgghm2  15052  mulgrhm  15053  zlmval  15071  znval  15080  asclghm  15134  assamulgscmlem1  15150  assamulgscm  15152  psrval  15159  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplvalcoe  15206  cnfval  15420  cnpfval  15421  ispsmet  15549  psmet0  15553  psmettri2  15554  psmetres2  15559  ismet  15570  isxmet  15571  xmettri2  15587  xmetres2  15605  xblss2  15631  xmstri2  15696  mstri2  15697  xmstri  15698  mstri  15699  xmstri3  15700  mstri3  15701  msrtri  15702  comet  15725  bdxmet  15727  txmetcnp  15744  metcnpd  15746  cnmet  15756  ioo2bl  15777  mpomulcn  15792  fsumcncntop  15793  elcncf  15799  mulc1cncf  15815  cncfco  15817  cncfcncntop  15819  cncfmptc  15822  cncfmptid  15823  addccncf  15826  cdivcncfap  15830  negcncf  15831  mulcncflem  15833  limccnp2cntop  15903  reldvg  15905  dvfvalap  15907  eldvap  15908  dvconst  15920  dvconstre  15922  dvconstss  15924  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvexp  15937  dvrecap  15939  dvmptid  15942  dvmptc  15943  dveflem  15952  dvef  15953  elplyd  15967  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plyadd  15977  plymul  15978  plycoeid3  15983  plycolemc  15984  plyco  15985  plycjlemc  15986  plycj  15987  plyrecj  15989  dvply1  15991  dvply2g  15992  sinperlem  16035  sinmpi  16042  cosmpi  16043  sinppi  16044  cosppi  16045  efimpi  16046  sinhalfpip  16047  sinhalfpim  16048  coshalfpip  16049  coshalfpim  16050  ptolemy  16051  tangtx  16065  logdivlti  16111  rpcxpadd  16138  rpmulcxp  16142  efnthr  16176  rplogbchbase  16186  rprelogbmul  16191  binom4  16219  log2tlbndlog2  16220  log2ublem2  16222  birthdaylem2  16226  pellexlem2  16230  pellexlem3  16231  wilthlem1  16232  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  1sgmprm  16288  1sgm2ppw  16289  sgmmul  16290  ppiqub  16293  chtublem  16295  chtqub  16296  mersenne  16297  perfect1  16298  perfectlem2  16300  perfect  16301  bcmono  16304  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  bposlem2  16312  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsdilem  16351  lgsdirprm  16358  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  gausslemma2dlem4  16388  gausslemma2dlem6  16391  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  lgsquad2lem2  16406  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2sqlem2  16439  2sqlem3  16441  2sqlem4  16442  2sqlem8  16447  vtxdgfval  16734  vtxdgfifival  16737  vtxdgop  16738  vtxdgfi0e  16741  vtxdeqd  16742  vtxdfifiun  16743  vtxduspgrfvedgfi  16747  1loopgrvd2fi  16751  repiecele0  17281  repiecege0  17282  repiecef  17283  cvgcmp2nlemabs  17287  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trilpo  17299  redcwlpo  17312  nconstwlpolemgt0  17321  nconstwlpo  17323  neapmkv  17325