Theorem oveq12d 5985

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 5976	. 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 5967

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq123d  5988  ovmpodxf  6094  ovmpodf  6100  caovdig  6144  caovdir2d  6146  caovdirg  6147  caovdilemd  6161  caovlem2d  6162  offval  6189  ofvalg  6191  offval2  6197  ofco  6200  caofinvl  6207  offres  6243  nnmsucr  6597  nndir  6599  ecovdi  6756  ecovidi  6757  dfplpq2  7502  dfmpq2  7503  addcmpblnq  7515  mulpipqqs  7521  addassnqg  7530  distrnqg  7535  ltaddnq  7555  halfnqq  7558  enq0tr  7582  addcmpblnq0  7591  addnq0mo  7595  addnnnq0  7597  nqnq0a  7602  distrnq0  7607  addassnq0  7610  distnq0r  7611  nq02m  7613  ltexpri  7761  cauappcvgprlemm  7793  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlem2  7808  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemmu  7843  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem2  7858  mulcmpblnrlemg  7888  mulsrmo  7892  mulsrpr  7894  mulcomsrg  7905  distrsrg  7907  recexgt0sr  7921  mulgt0sr  7926  mulextsr1lem  7928  caucvgsrlemgt1  7943  caucvgsr  7950  addcnsr  7982  mulcnsr  7983  recidpirqlemcalc  8005  axaddcl  8012  axmulcl  8014  axmulcom  8019  axmulass  8021  axdistr  8022  axcaucvglemcau  8046  axcaucvglemres  8047  adddir  8098  muladd11  8240  1p1times  8241  muladd11r  8263  pnpcan2  8347  muladd  8491  subdir  8493  mulsub  8508  mulreim  8712  apadd1  8716  mulext1  8720  recextlem1  8759  muleqadd  8776  divdirap  8805  divadddivap  8835  conjmulap  8837  divcanap5rd  8926  subrecap  8947  xp1d2m1eqxm1d2  9325  div4p1lem1div2  9326  cnref1o  9807  xnegid  10016  xposdif  10039  xleaddadd  10044  icoshftf1o  10148  lincmb01cmp  10160  iccf1o  10161  fz01en  10210  fzrev3  10244  fzrevral2  10263  fzrevral3  10264  fzshftral  10265  fzoaddel2  10356  fzosubel  10360  fzosubel2  10361  fzocatel  10365  modqsubdir  10575  addmodlteq  10580  frecuzrdgsuc  10596  frecfzen2  10609  iseqovex  10640  seqvalcd  10643  seq3caopr3  10673  seqcaopr3g  10674  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seqf1oglem2  10702  seq3id3  10706  seqfeq3  10711  seq3distr  10714  ser3le  10719  mulexp  10760  mulexpzap  10761  expaddzap  10765  expubnd  10778  subsq  10828  binom2  10833  binom21  10834  binom2sub  10835  binom2sub1  10836  binom3  10839  sqoddm1div8  10875  mulsubdivbinom2ap  10893  nn0opthlem1d  10902  nn0opthd  10904  facp1  10912  facubnd  10927  bcval  10931  bcn1  10940  bcm1k  10942  bcp1n  10943  bcp1nk  10944  bcval5  10945  bcn2  10946  bcpasc  10948  hashun  10987  hashfz  11003  ccatlid  11100  ccatass  11102  ccat1st1st  11131  swrdval  11139  swrdspsleq  11158  ccatswrd  11161  pfxval  11165  addlenpfx  11182  ccatpfx  11192  ccatopth  11207  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  swrdccat  11226  swrdccat3blem  11230  swrdccatin2d  11235  pfxccatin12d  11236  crre  11283  replim  11285  remullem  11297  remul2  11299  immul2  11306  cjcj  11309  cjadd  11310  ipcnval  11312  cjmulval  11314  cjneg  11316  imval2  11320  cjreim  11329  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrexlemcalc1  11440  resqrexlemcalc2  11441  resqrex  11452  sqabsadd  11481  sqabssub  11482  absreimsq  11493  recan  11535  amgm2  11544  maxabslemab  11632  maxabslemval  11634  max0addsup  11645  minabs  11662  bdtrilem  11665  bdtri  11666  xrmaxadd  11687  xrminadd  11701  xrbdtri  11702  subcn2  11737  reccn2ap  11739  climle  11760  climcvg1nlem  11775  serf0  11778  fsumadd  11832  fsumsplit  11833  sumpr  11839  sumtp  11840  isumadd  11857  sumsplitdc  11858  fsum2dlemstep  11860  fsumshftm  11871  fisumrev2  11872  fsumconst  11880  modfsummodlemstep  11883  telfsumo  11892  fsumparts  11896  binomlem  11909  binom  11910  binom1dif  11913  bcxmaslem1  11914  isumsplit  11917  isumnn0nn  11919  arisum  11924  arisum2  11925  trireciplem  11926  trirecip  11927  geosergap  11932  geo2sum  11940  geo2sum2  11941  cvgratnnlemsumlt  11954  mertenslemi1  11961  mertensabs  11963  fprodmul  12017  fprodsplitdc  12022  fprodabs  12042  fprod2dlemstep  12048  fproddivapf  12057  eftabs  12082  eftvalcn  12083  efcllemp  12084  ege2le3  12097  efcj  12099  efaddlem  12100  efsep  12117  ef4p  12120  efgt1p2  12121  efgt1p  12122  sinval  12128  cosval  12129  tanvalap  12134  tanval2ap  12139  tanval3ap  12140  efi4p  12143  sinneg  12152  cosneg  12153  tannegap  12154  efival  12158  efmival  12159  sinadd  12162  cosadd  12163  tanaddaplem  12164  tanaddap  12165  sinsub  12166  cossub  12167  addsin  12168  subsin  12169  sinmul  12170  cosmul  12171  addcos  12172  subcos  12173  sincossq  12174  cos2t  12176  sin01bnd  12183  cos01bnd  12184  efieq1re  12198  demoivreALT  12200  dvds2ln  12250  odd2np1lem  12298  bitsinv1lem  12387  gcdaddm  12420  bezoutlemnewy  12432  dfgcd3  12446  dvdsgcd  12448  mulgcd  12452  mulgcdr  12454  gcddiv  12455  sqgcd  12465  lcmgcdlem  12514  lcmgcd  12515  qredeu  12534  divgcdcoprm0  12538  cncongr1  12540  oddpwdclemdc  12610  sqrt2irraplemnn  12616  qnumdenbi  12629  zgcdsq  12638  hashdvds  12658  phiprmpw  12659  phimullem  12662  eulerthlema  12667  prmdiv  12672  modprm0  12692  coprimeprodsq  12695  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  pythagtriplem19  12720  pcval  12734  pcmul  12739  pcdiv  12740  pcqmul  12741  pcid  12762  pcaddlem  12777  pcmpt  12781  pcmpt2  12782  pcmptdvds  12783  pcbc  12789  4sqlem4  12830  mul4sqlem  12831  mul4sq  12832  4sqlem11  12839  4sqlem12  12840  4sqlem15  12843  4sqlem17  12845  ennnfonelemp1  12892  nninfdclemp1  12936  ressvalsets  13011  topnvalg  13198  topnpropgd  13200  prdsex  13216  prdsval  13220  pwsval  13238  qusval  13270  qusex  13272  qusaddvallemg  13280  xpsval  13299  gsumprval  13346  imasmnd2  13399  ismhm  13408  mhmf1o  13417  0mhm  13433  mhmco  13437  mhmeql  13439  gsumfzz  13442  isgrpid2  13487  grpnpcan  13539  imasgrp2  13561  mhmmnd  13567  mulgnndir  13602  mulgdir  13605  isnsg3  13658  isghm  13694  ghmnsgima  13719  ghmf1o  13726  conjghm  13727  qusghm  13733  ablsub4  13764  ghmcmn  13778  invghm  13780  gsumfzmptfidmadd  13790  gsumfzconst  13792  mgpvalg  13800  mgptopng  13806  mgpress  13808  rngdi  13817  rngdir  13818  rngpropd  13832  imasrng  13833  srglmhm  13870  srgrmhm  13871  ringo2times  13905  ringcom  13908  ringpropd  13915  ring1  13936  ringlghm  13938  ringrghm  13939  imasring  13941  opprvalg  13946  opprrng  13954  opprring  13956  invrfvald  13999  dvrvald  14011  dvrdir  14020  rdivmuldivd  14021  islmod  14168  lmodlema  14169  islmodd  14170  lmodcom  14210  lmodnegadd  14213  lmodprop2d  14225  rmodislmod  14228  lsssn0  14247  sraval  14314  qusrhm  14405  gsumfzfsumlemm  14464  expghmap  14484  mulgghm2  14485  mulgrhm  14486  zlmval  14504  znval  14513  psrval  14543  mplvalcoe  14567  cnfval  14781  cnpfval  14782  ispsmet  14910  psmet0  14914  psmettri2  14915  psmetres2  14920  ismet  14931  isxmet  14932  xmettri2  14948  xmetres2  14966  xblss2  14992  xmstri2  15057  mstri2  15058  xmstri  15059  mstri  15060  xmstri3  15061  mstri3  15062  msrtri  15063  comet  15086  bdxmet  15088  txmetcnp  15105  metcnpd  15107  cnmet  15117  ioo2bl  15138  mpomulcn  15153  fsumcncntop  15154  elcncf  15160  mulc1cncf  15176  cncfco  15178  cncfcncntop  15180  cncfmptc  15183  cncfmptid  15184  addccncf  15187  cdivcncfap  15191  negcncf  15192  mulcncflem  15194  limccnp2cntop  15264  reldvg  15266  dvfvalap  15268  eldvap  15269  dvconst  15281  dvconstre  15283  dvconstss  15285  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvexp  15298  dvrecap  15300  dvmptid  15303  dvmptc  15304  dveflem  15313  dvef  15314  elplyd  15328  ply1termlem  15329  plyaddlem1  15334  plymullem1  15335  plyadd  15338  plymul  15339  plycoeid3  15344  plycolemc  15345  plyco  15346  plycjlemc  15347  plycj  15348  plyrecj  15350  dvply1  15352  dvply2g  15353  sinperlem  15395  sinmpi  15402  cosmpi  15403  sinppi  15404  cosppi  15405  efimpi  15406  sinhalfpip  15407  sinhalfpim  15408  coshalfpip  15409  coshalfpim  15410  ptolemy  15411  tangtx  15425  logdivlti  15468  rpcxpadd  15492  rpmulcxp  15496  rplogbchbase  15537  rprelogbmul  15542  binom4  15566  wilthlem1  15567  1sgmprm  15581  1sgm2ppw  15582  sgmmul  15583  mersenne  15584  perfect1  15585  perfectlem2  15587  perfect  15588  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsval4a  15614  lgsneg  15616  lgsdilem  15619  lgsdirprm  15626  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  gausslemma2dlem4  15656  gausslemma2dlem6  15659  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad2lem2  15674  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2sqlem2  15707  2sqlem3  15709  2sqlem4  15710  2sqlem8  15715  cvgcmp2nlemabs  16173  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trilpo  16184  redcwlpo  16196  nconstwlpolemgt0  16205  nconstwlpo  16207  neapmkv  16209