Theorem oveq12d 6076

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 6067	. 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 6058

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 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq123d  6079  ovmpodxf  6187  ovmpodf  6193  caovdig  6237  caovdir2d  6239  caovdirg  6240  caovdilemd  6254  caovlem2d  6255  offval  6283  ofvalg  6285  offval2  6291  ofco  6294  caofinvl  6301  offres  6341  nnmsucr  6734  nndir  6736  ecovdi  6893  ecovidi  6894  dfplpq2  7685  dfmpq2  7686  addcmpblnq  7698  mulpipqqs  7704  addassnqg  7713  distrnqg  7718  ltaddnq  7738  halfnqq  7741  enq0tr  7765  addcmpblnq0  7774  addnq0mo  7778  addnnnq0  7780  nqnq0a  7785  distrnq0  7790  addassnq0  7793  distnq0r  7794  nq02m  7796  ltexpri  7944  cauappcvgprlemm  7976  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemmu  8026  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem2  8041  mulcmpblnrlemg  8071  mulsrmo  8075  mulsrpr  8077  mulcomsrg  8088  distrsrg  8090  recexgt0sr  8104  mulgt0sr  8109  mulextsr1lem  8111  caucvgsrlemgt1  8126  caucvgsr  8133  addcnsr  8165  mulcnsr  8166  recidpirqlemcalc  8188  axaddcl  8195  axmulcl  8197  axmulcom  8202  axmulass  8204  axdistr  8205  axcaucvglemcau  8229  axcaucvglemres  8230  adddir  8281  muladd11  8423  1p1times  8424  muladd11r  8446  pnpcan2  8530  muladd  8675  subdir  8677  mulsub  8692  mulreim  8896  apadd1  8900  mulext1  8904  recextlem1  8943  muleqadd  8962  divdirap  8991  divadddivap  9021  conjmulap  9023  divcanap5rd  9112  subrecap  9133  xp1d2m1eqxm1d2  9511  div4p1lem1div2  9512  cnref1o  10004  xnegid  10214  xposdif  10237  xleaddadd  10242  icoshftf1o  10346  lincmb01cmp  10358  iccf1o  10360  fz01en  10411  fzrev3  10446  fzrevral2  10465  fzrevral3  10466  fzshftral  10467  fzoaddel2  10560  fzosubel  10564  fzosubel2  10565  fzocatel  10569  modqsubdir  10782  addmodlteq  10787  frecuzrdgsuc  10803  frecfzen2  10816  iseqovex  10847  seqvalcd  10850  seq3caopr3  10880  seqcaopr3g  10881  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seqf1oglem2  10909  seq3id3  10913  seqfeq3  10918  seq3distr  10921  ser3le  10926  mulexp  10967  mulexpzap  10968  expaddzap  10972  expubnd  10985  subsq  11035  binom2  11040  binom21  11041  binom2sub  11042  binom2sub1  11043  binom3  11046  sqoddm1div8  11083  mulsubdivbinom2ap  11101  nn0opthlem1d  11110  nn0opthd  11112  facp1  11120  facubnd  11135  bcval  11139  bcn1  11148  bcm1k  11150  bcp1n  11151  bcp1nk  11152  bcval5  11153  bcn2  11154  bcpasc  11156  bcm1n  11159  hashun  11197  hashfz  11214  hashfibclem  11234  hashfibc  11235  hashtpgim  11245  ccatlid  11322  ccatass  11324  ccat1st1st  11357  swrdval  11368  swrdspsleq  11387  ccatswrd  11390  pfxval  11394  addlenpfx  11411  ccatpfx  11421  ccatopth  11436  pfxccatin12lem1  11448  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12  11453  swrdccat  11455  swrdccat3blem  11459  swrdccatin2d  11464  pfxccatin12d  11465  cats1lend  11487  cats2catd  11489  s2eqd  11490  s3eqd  11491  s4eqd  11492  s5eqd  11493  s6eqd  11494  s7eqd  11495  s8eqd  11496  crre  11570  replim  11572  remullem  11584  remul2  11586  immul2  11593  cjcj  11596  cjadd  11597  ipcnval  11599  cjmulval  11601  cjneg  11603  imval2  11607  cjreim  11616  cvg1nlemcau  11697  cvg1nlemres  11698  resqrexlemp1rp  11719  resqrexlemfp1  11722  resqrexlemcalc1  11727  resqrexlemcalc2  11728  resqrex  11739  sqabsadd  11768  sqabssub  11769  absreimsq  11780  recan  11822  amgm2  11831  maxabslemab  11919  maxabslemval  11921  max0addsup  11932  minabs  11949  bdtrilem  11952  bdtri  11953  xrmaxadd  11974  xrminadd  11988  xrbdtri  11989  subcn2  12024  reccn2ap  12026  climle  12047  climcvg1nlem  12062  serf0  12065  fsumadd  12120  fsumsplit  12121  sumpr  12127  sumtp  12128  isumadd  12145  sumsplitdc  12146  fsum2dlemstep  12148  fsumshftm  12159  fisumrev2  12160  fsumconst  12168  modfsummodlemstep  12171  telfsumo  12180  fsumparts  12184  binomlem  12197  binom  12198  binom1dif  12201  bcxmaslem1  12202  isumsplit  12205  isumnn0nn  12207  arisum  12212  arisum2  12213  trireciplem  12214  trirecip  12215  geosergap  12220  geo2sum  12228  geo2sum2  12229  cvgratnnlemsumlt  12242  mertenslemi1  12249  mertensabs  12251  fprodmul  12305  fprodsplitdc  12310  fprodabs  12330  fprod2dlemstep  12336  fproddivapf  12345  eftabs  12370  eftvalcn  12371  efcllemp  12372  ege2le3  12385  efcj  12387  efaddlem  12388  efsep  12405  ef4p  12408  efgt1p2  12409  efgt1p  12410  sinval  12416  cosval  12417  tanvalap  12422  tanval2ap  12427  tanval3ap  12428  efi4p  12431  sinneg  12440  cosneg  12441  tannegap  12442  efival  12446  efmival  12447  sinadd  12450  cosadd  12451  tanaddaplem  12452  tanaddap  12453  sinsub  12454  cossub  12455  addsin  12456  subsin  12457  sinmul  12458  cosmul  12459  addcos  12460  subcos  12461  sincossq  12462  cos2t  12464  sin01bnd  12471  cos01bnd  12472  efieq1re  12486  demoivreALT  12488  dvds2ln  12538  odd2np1lem  12586  bitsinv1lem  12675  gcdaddm  12708  bezoutlemnewy  12720  dfgcd3  12734  dvdsgcd  12736  mulgcd  12740  mulgcdr  12742  gcddiv  12743  sqgcd  12753  lcmgcdlem  12802  lcmgcd  12803  qredeu  12822  divgcdcoprm0  12826  cncongr1  12828  oddpwdclemdc  12898  sqrt2irraplemnn  12904  qnumdenbi  12917  zgcdsq  12926  hashdvds  12946  phiprmpw  12947  phimullem  12950  eulerthlema  12955  prmdiv  12960  modprm0  12980  coprimeprodsq  12983  pythagtriplem1  12991  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem15  13004  pythagtriplem16  13005  pythagtriplem17  13006  pythagtriplem19  13008  pcval  13022  pcmul  13027  pcdiv  13028  pcqmul  13029  pcid  13050  pcaddlem  13065  pcmpt  13069  pcmpt2  13070  pcmptdvds  13071  pcbc  13077  4sqlem4  13118  mul4sqlem  13119  mul4sq  13120  4sqlem11  13127  4sqlem12  13128  4sqlem15  13131  4sqlem17  13133  ballotfilemfval  13176  ballotfilemfp1  13178  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemfmpn  13181  ballotfilemgval  13214  ballotfilemgun  13215  ballotfilemfrc  13217  ballotfilemfrceq  13219  ennnfonelemp1  13244  nninfdclemp1  13288  ressvalsets  13364  topnvalg  13551  topnpropgd  13553  qusval  13590  qusex  13592  qusaddvallemg  13600  gsumprval  13665  imasmnd2  13710  ismhm  13719  mhmf1o  13728  0mhm  13744  mhmco  13748  mhmeql  13750  gsumfzz  13753  isgrpid2  13798  grpnpcan  13850  imasgrp2  13866  mhmmnd  13872  mulgnndir  13907  mulgdir  13910  isnsg3  13963  isghm  13999  ghmnsgima  14024  ghmf1o  14031  conjghm  14032  qusghm  14038  ablsub4  14069  ghmcmn  14083  invghm  14085  gsumfzmptfidmadd  14095  gsumfzconst  14097  gsumgfsum  14109  gfsump1  14111  gfsumz  14112  prdsex  14117  prdsval  14118  xpsval  14146  pwsval  14149  mgpvalg  14165  mgptopng  14171  mgpress  14173  rngdi  14182  rngdir  14183  rngpropd  14197  imasrng  14198  srglmhm  14239  srgrmhm  14240  ringo2times  14274  ringcom  14277  ringpropd  14284  ring1  14305  ringlghm  14307  ringrghm  14308  imasring  14310  opprvalg  14315  opprrng  14323  opprring  14325  invrfvald  14370  dvrvald  14382  dvrdir  14391  rdivmuldivd  14392  islmod  14568  lmodlema  14569  islmodd  14570  lmodcom  14610  lmodnegadd  14613  lmodprop2d  14625  rmodislmod  14628  lsssn0  14647  sraval  14714  qusrhm  14805  gsumfzfsumlemm  14864  expghmap  14884  mulgghm2  14885  mulgrhm  14886  zlmval  14904  znval  14913  psrval  14943  mplvalcoe  14974  cnfval  15188  cnpfval  15189  ispsmet  15317  psmet0  15321  psmettri2  15322  psmetres2  15327  ismet  15338  isxmet  15339  xmettri2  15355  xmetres2  15373  xblss2  15399  xmstri2  15464  mstri2  15465  xmstri  15466  mstri  15467  xmstri3  15468  mstri3  15469  msrtri  15470  comet  15493  bdxmet  15495  txmetcnp  15512  metcnpd  15514  cnmet  15524  ioo2bl  15545  mpomulcn  15560  fsumcncntop  15561  elcncf  15567  mulc1cncf  15583  cncfco  15585  cncfcncntop  15587  cncfmptc  15590  cncfmptid  15591  addccncf  15594  cdivcncfap  15598  negcncf  15599  mulcncflem  15601  limccnp2cntop  15671  reldvg  15673  dvfvalap  15675  eldvap  15676  dvconst  15688  dvconstre  15690  dvconstss  15692  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvexp  15705  dvrecap  15707  dvmptid  15710  dvmptc  15711  dveflem  15720  dvef  15721  elplyd  15735  ply1termlem  15736  plyaddlem1  15741  plymullem1  15742  plyadd  15745  plymul  15746  plycoeid3  15751  plycolemc  15752  plyco  15753  plycjlemc  15754  plycj  15755  plyrecj  15757  dvply1  15759  dvply2g  15760  sinperlem  15802  sinmpi  15809  cosmpi  15810  sinppi  15811  cosppi  15812  efimpi  15813  sinhalfpip  15814  sinhalfpim  15815  coshalfpip  15816  coshalfpim  15817  ptolemy  15818  tangtx  15832  logdivlti  15875  rpcxpadd  15899  rpmulcxp  15903  rplogbchbase  15944  rprelogbmul  15949  binom4  15973  pellexlem2  15975  pellexlem3  15976  wilthlem1  15977  1sgmprm  15991  1sgm2ppw  15992  sgmmul  15993  mersenne  15994  perfect1  15995  perfectlem2  15997  perfect  15998  lgsval  16006  lgsfvalg  16007  lgsval2lem  16012  lgsval4a  16024  lgsneg  16026  lgsdilem  16029  lgsdirprm  16036  lgsdir  16037  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  gausslemma2dlem4  16066  gausslemma2dlem6  16069  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2lem1  16083  lgsquad2lem2  16084  2lgslem3a  16095  2lgslem3b  16096  2lgslem3c  16097  2lgslem3d  16098  2sqlem2  16117  2sqlem3  16119  2sqlem4  16120  2sqlem8  16125  vtxdgfval  16412  vtxdgfifival  16415  vtxdgop  16416  vtxdgfi0e  16419  vtxdeqd  16420  vtxdfifiun  16421  vtxduspgrfvedgfi  16425  1loopgrvd2fi  16429  repiecele0  16949  repiecege0  16950  repiecef  16951  cvgcmp2nlemabs  16955  trilpolemclim  16959  trilpolemcl  16960  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964  trilpo  16966  redcwlpo  16979  nconstwlpolemgt0  16989  nconstwlpo  16991  neapmkv  16993