Theorem oveq12d 6103

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 6094	. 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 6085

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123d  6106  ovmpodxf  6214  ovmpodf  6220  caovdig  6264  caovdir2d  6266  caovdirg  6267  caovdilemd  6281  caovlem2d  6282  offval  6310  ofvalg  6312  offval2  6318  ofco  6321  caofinvl  6328  offres  6368  nnmsucr  6761  nndir  6763  ecovdi  6920  ecovidi  6921  dfplpq2  7721  dfmpq2  7722  addcmpblnq  7734  mulpipqqs  7740  addassnqg  7749  distrnqg  7754  ltaddnq  7774  halfnqq  7777  enq0tr  7801  addcmpblnq0  7810  addnq0mo  7814  addnnnq0  7816  nqnq0a  7821  distrnq0  7826  addassnq0  7829  distnq0r  7830  nq02m  7832  ltexpri  7980  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemmu  8062  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem2  8077  mulcmpblnrlemg  8107  mulsrmo  8111  mulsrpr  8113  mulcomsrg  8124  distrsrg  8126  recexgt0sr  8140  mulgt0sr  8145  mulextsr1lem  8147  caucvgsrlemgt1  8162  caucvgsr  8169  addcnsr  8201  mulcnsr  8202  recidpirqlemcalc  8224  axaddcl  8231  axmulcl  8233  axmulcom  8238  axmulass  8240  axdistr  8241  axcaucvglemcau  8265  axcaucvglemres  8266  adddir  8317  muladd11  8459  1p1times  8460  muladd11r  8482  pnpcan2  8566  muladd  8711  subdir  8713  mulsub  8728  mulreim  8932  apadd1  8936  mulext1  8940  recextlem1  8979  muleqadd  8998  divdirap  9027  divadddivap  9057  conjmulap  9059  divcanap5rd  9148  subrecap  9169  xp1d2m1eqxm1d2  9558  div4p1lem1div2  9559  cnref1o  10051  xnegid  10261  xposdif  10284  xleaddadd  10289  icoshftf1o  10393  lincmb01cmp  10405  iccf1o  10407  fz01en  10459  fzrev3  10494  fzrevral2  10513  fzrevral3  10514  fzshftral  10515  fzoaddel2  10608  fzosubel  10612  fzosubel2  10613  fzocatel  10617  modqsubdir  10830  addmodlteq  10835  frecuzrdgsuc  10851  frecfzen2  10864  iseqovex  10895  seqvalcd  10898  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seqf1oglem2  10957  seq3id3  10961  seqfeq3  10966  seq3distr  10969  ser3le  10974  mulexp  11015  mulexpzap  11016  expaddzap  11020  expubnd  11033  subsq  11083  binom2  11088  binom21  11089  binom2sub  11090  binom2sub1  11091  binom3  11094  sqoddm1div8  11131  mulsubdivbinom2ap  11149  nn0opthlem1d  11158  nn0opthd  11160  facp1  11168  facubnd  11183  bcval  11187  bcn1  11196  bcm1k  11198  bcp1n  11199  bcp1nk  11200  bcval5  11201  bcn2  11202  bcpasc  11204  bcm1n  11207  hashun  11245  hashfz  11262  hashfibclem  11282  hashfibc  11283  hashf1lem2  11286  hashf1  11287  hashtpgim  11297  ccatlid  11374  ccatass  11376  ccat1st1st  11409  swrdval  11420  swrdspsleq  11439  ccatswrd  11442  pfxval  11446  addlenpfx  11463  ccatpfx  11473  ccatopth  11488  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccat  11507  swrdccat3blem  11511  swrdccatin2d  11516  pfxccatin12d  11517  cats1lend  11539  cats2catd  11541  s2eqd  11542  s3eqd  11543  s4eqd  11544  s5eqd  11545  s6eqd  11546  s7eqd  11547  s8eqd  11548  crre  11622  replim  11624  remullem  11636  remul2  11638  immul2  11645  cjcj  11648  cjadd  11649  ipcnval  11651  cjmulval  11653  cjneg  11655  imval2  11659  cjreim  11669  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrexlemcalc1  11780  resqrexlemcalc2  11781  resqrex  11792  sqabsadd  11821  sqabssub  11822  absreimsq  11833  recan  11875  amgm2  11884  maxabslemab  11972  maxabslemval  11974  max0addsup  11985  minabs  12002  bdtrilem  12005  bdtri  12006  xrmaxadd  12027  xrminadd  12041  xrbdtri  12042  subcn2  12077  reccn2ap  12079  climle  12100  climcvg1nlem  12115  serf0  12118  fsumadd  12173  fsumsplit  12174  sumpr  12180  sumtp  12181  isumadd  12198  sumsplitdc  12199  fsum2dlemstep  12201  fsumshftm  12212  fisumrev2  12213  fsumconst  12221  modfsummodlemstep  12224  telfsumo  12233  fsumparts  12237  binomlem  12250  binom  12251  binom1dif  12254  bcxmaslem1  12255  isumsplit  12258  isumnn0nn  12260  arisum  12265  arisum2  12266  trireciplem  12267  trirecip  12268  geosergap  12273  geo2sum  12281  geo2sum2  12282  cvgratnnlemsumlt  12295  mertenslemi1  12302  mertensabs  12304  fprodmul  12358  fprodsplitdc  12363  fprodabs  12383  fprod2dlemstep  12389  fproddivapf  12398  eftabs  12423  eftvalcn  12424  efcllemp  12425  ege2le3  12438  efcj  12440  efaddlem  12441  efsep  12458  ef4p  12461  efgt1p2  12462  efgt1p  12463  sinval  12469  cosval  12470  tanvalap  12475  tanval2ap  12480  tanval3ap  12481  efi4p  12484  sinneg  12493  cosneg  12494  tannegap  12495  efival  12499  efmival  12500  sinadd  12503  cosadd  12504  tanaddaplem  12505  tanaddap  12506  sinsub  12507  cossub  12508  addsin  12509  subsin  12510  sinmul  12511  cosmul  12512  addcos  12513  subcos  12514  sincossq  12515  cos2t  12517  sin01bnd  12524  cos01bnd  12525  efieq1re  12539  demoivreALT  12541  dvds2ln  12591  odd2np1lem  12639  bitsinv1lem  12728  gcdaddm  12761  bezoutlemnewy  12773  dfgcd3  12787  dvdsgcd  12789  mulgcd  12793  mulgcdr  12795  gcddiv  12796  sqgcd  12806  lcmgcdlem  12855  lcmgcd  12856  qredeu  12875  divgcdcoprm0  12879  cncongr1  12881  oddpwdclemdc  12951  sqrt2irraplemnn  12957  qnumdenbi  12970  zgcdsq  12979  hashdvds  12999  phiprmpw  13000  phimullem  13003  eulerthlema  13008  prmdiv  13013  modprm0  13033  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  pythagtriplem19  13061  pcval  13075  pcmul  13080  pcdiv  13081  pcqmul  13082  pcid  13103  pcaddlem  13118  pcmpt  13122  pcmpt2  13123  pcmptdvds  13124  pcbc  13130  4sqlem4  13171  mul4sqlem  13172  mul4sq  13173  4sqlem11  13180  4sqlem12  13181  4sqlem15  13184  4sqlem17  13186  ballotfilemfval  13229  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfmpn  13234  ballotfilemgval  13267  ballotfilemgun  13268  ballotfilemfrc  13270  ballotfilemfrceq  13272  ennnfonelemp1  13297  nninfdclemp1  13341  ressvalsets  13418  topnvalg  13605  topnpropgd  13607  qusval  13644  qusex  13646  qusaddvallemg  13654  imasmnd2  13759  ismhm  13768  mhmf1o  13777  0mhm  13793  mhmco  13797  mhmeql  13799  isgrpid2  13845  grpnpcan  13897  imasgrp2  13913  mhmmnd  13919  mulgnndir  13954  mulgdir  13957  isnsg3  14010  isghm  14046  ghmnsgima  14071  ghmf1o  14078  conjghm  14079  qusghm  14085  ablsub4  14117  ghmcmn  14131  invghm  14133  gzsumconst  14143  gzsumgsum  14155  gsump1  14157  gsumzfi  14158  gsummptfidmadd  14161  gsumconstcmn  14166  prdsex  14172  prdsval  14173  xpsval  14201  pwsval  14204  mgpvalg  14220  mgptopng  14228  mgpress  14230  rngdi  14239  rngdir  14240  rngpropd  14254  imasrng  14255  srglmhm  14297  srgrmhm  14298  ringo2times  14333  ringcom  14336  ringpropd  14343  ring1  14364  ringlghm  14366  ringrghm  14367  imasring  14369  opprvalg  14374  opprrng  14382  opprring  14384  invrfvald  14429  dvrvald  14441  dvrdir  14450  rdivmuldivd  14451  islmod  14627  lmodlema  14628  islmodd  14629  lmodcom  14670  lmodnegadd  14673  lmodprop2d  14685  rmodislmod  14688  lsssn0  14707  sraval  14774  qusrhm  14865  gsumfsum  14923  expghmap  14942  mulgghm2  14943  mulgrhm  14944  zlmval  14962  znval  14971  asclghm  15025  assamulgscmlem1  15041  assamulgscm  15043  psrval  15050  mplvalcoe  15081  cnfval  15295  cnpfval  15296  ispsmet  15424  psmet0  15428  psmettri2  15429  psmetres2  15434  ismet  15445  isxmet  15446  xmettri2  15462  xmetres2  15480  xblss2  15506  xmstri2  15571  mstri2  15572  xmstri  15573  mstri  15574  xmstri3  15575  mstri3  15576  msrtri  15577  comet  15600  bdxmet  15602  txmetcnp  15619  metcnpd  15621  cnmet  15631  ioo2bl  15652  mpomulcn  15667  fsumcncntop  15668  elcncf  15674  mulc1cncf  15690  cncfco  15692  cncfcncntop  15694  cncfmptc  15697  cncfmptid  15698  addccncf  15701  cdivcncfap  15705  negcncf  15706  mulcncflem  15708  limccnp2cntop  15778  reldvg  15780  dvfvalap  15782  eldvap  15783  dvconst  15795  dvconstre  15797  dvconstss  15799  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvexp  15812  dvrecap  15814  dvmptid  15817  dvmptc  15818  dveflem  15827  dvef  15828  elplyd  15842  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plyadd  15852  plymul  15853  plycoeid3  15858  plycolemc  15859  plyco  15860  plycjlemc  15861  plycj  15862  plyrecj  15864  dvply1  15866  dvply2g  15867  sinperlem  15909  sinmpi  15916  cosmpi  15917  sinppi  15918  cosppi  15919  efimpi  15920  sinhalfpip  15921  sinhalfpim  15922  coshalfpip  15923  coshalfpim  15924  ptolemy  15925  tangtx  15939  logdivlti  15982  rpcxpadd  16007  rpmulcxp  16011  rplogbchbase  16052  rprelogbmul  16057  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  birthdaylem2  16088  pellexlem2  16092  pellexlem3  16093  wilthlem1  16094  1sgmprm  16108  1sgm2ppw  16109  sgmmul  16110  mersenne  16111  perfect1  16112  perfectlem2  16114  perfect  16115  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsval4a  16141  lgsneg  16143  lgsdilem  16146  lgsdirprm  16153  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  gausslemma2dlem4  16183  gausslemma2dlem6  16186  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  lgsquad2lem2  16201  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2sqlem2  16234  2sqlem3  16236  2sqlem4  16237  2sqlem8  16242  vtxdgfval  16529  vtxdgfifival  16532  vtxdgop  16533  vtxdgfi0e  16536  vtxdeqd  16537  vtxdfifiun  16538  vtxduspgrfvedgfi  16542  1loopgrvd2fi  16546  repiecele0  17075  repiecege0  17076  repiecef  17077  cvgcmp2nlemabs  17081  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trilpo  17092  redcwlpo  17105  nconstwlpolemgt0  17114  nconstwlpo  17116  neapmkv  17118