Theorem oveq12d 6096

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 6087	. 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 ) )

Syntax hints:   -> wi 4   = wceq 1402  (class class class)co 6078

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081

This theorem is referenced by:  oveq123d  6099  ovmpodxf  6207  ovmpodf  6213  caovdig  6257  caovdir2d  6259  caovdirg  6260  caovdilemd  6274  caovlem2d  6275  offval  6303  ofvalg  6305  offval2  6311  ofco  6314  caofinvl  6321  offres  6361  nnmsucr  6754  nndir  6756  ecovdi  6913  ecovidi  6914  dfplpq2  7714  dfmpq2  7715  addcmpblnq  7727  mulpipqqs  7733  addassnqg  7742  distrnqg  7747  ltaddnq  7767  halfnqq  7770  enq0tr  7794  addcmpblnq0  7803  addnq0mo  7807  addnnnq0  7809  nqnq0a  7814  distrnq0  7819  addassnq0  7822  distnq0r  7823  nq02m  7825  ltexpri  7973  cauappcvgprlemm  8005  cauappcvgprlemloc  8012  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  cauappcvgprlem1  8019  cauappcvgprlem2  8020  cauappcvgprlemlim  8021  cauappcvgpr  8022  caucvgprlemnkj  8026  caucvgprlemnbj  8027  caucvgprlemm  8028  caucvgprlemloc  8035  caucvgprlemcl  8036  caucvgprlemladdfu  8037  caucvgprlemladdrl  8038  caucvgprlem2  8040  caucvgpr  8042  caucvgprprlemelu  8046  caucvgprprlemcbv  8047  caucvgprprlemval  8048  caucvgprprlemmu  8055  caucvgprprlemopu  8059  caucvgprprlemloc  8063  caucvgprprlemclphr  8065  caucvgprprlemexbt  8066  caucvgprprlem2  8070  mulcmpblnrlemg  8100  mulsrmo  8104  mulsrpr  8106  mulcomsrg  8117  distrsrg  8119  recexgt0sr  8133  mulgt0sr  8138  mulextsr1lem  8140  caucvgsrlemgt1  8155  caucvgsr  8162  addcnsr  8194  mulcnsr  8195  recidpirqlemcalc  8217  axaddcl  8224  axmulcl  8226  axmulcom  8231  axmulass  8233  axdistr  8234  axcaucvglemcau  8258  axcaucvglemres  8259  adddir  8310  muladd11  8452  1p1times  8453  muladd11r  8475  pnpcan2  8559  muladd  8704  subdir  8706  mulsub  8721  mulreim  8925  apadd1  8929  mulext1  8933  recextlem1  8972  muleqadd  8991  divdirap  9020  divadddivap  9050  conjmulap  9052  divcanap5rd  9141  subrecap  9162  xp1d2m1eqxm1d2  9540  div4p1lem1div2  9541  cnref1o  10033  xnegid  10243  xposdif  10266  xleaddadd  10271  icoshftf1o  10375  lincmb01cmp  10387  iccf1o  10389  fz01en  10440  fzrev3  10475  fzrevral2  10494  fzrevral3  10495  fzshftral  10496  fzoaddel2  10589  fzosubel  10593  fzosubel2  10594  fzocatel  10598  modqsubdir  10811  addmodlteq  10816  frecuzrdgsuc  10832  frecfzen2  10845  iseqovex  10876  seqvalcd  10879  seq3caopr3  10909  seqcaopr3g  10910  seq3f1olemqsumkj  10929  seq3f1olemqsumk  10930  seq3f1olemqsum  10931  seqf1oglem2  10938  seq3id3  10942  seqfeq3  10947  seq3distr  10950  ser3le  10955  mulexp  10996  mulexpzap  10997  expaddzap  11001  expubnd  11014  subsq  11064  binom2  11069  binom21  11070  binom2sub  11071  binom2sub1  11072  binom3  11075  sqoddm1div8  11112  mulsubdivbinom2ap  11130  nn0opthlem1d  11139  nn0opthd  11141  facp1  11149  facubnd  11164  bcval  11168  bcn1  11177  bcm1k  11179  bcp1n  11180  bcp1nk  11181  bcval5  11182  bcn2  11183  bcpasc  11185  bcm1n  11188  hashun  11226  hashfz  11243  hashfibclem  11263  hashfibc  11264  hashf1lem2  11267  hashf1  11268  hashtpgim  11278  ccatlid  11355  ccatass  11357  ccat1st1st  11390  swrdval  11401  swrdspsleq  11420  ccatswrd  11423  pfxval  11427  addlenpfx  11444  ccatpfx  11454  ccatopth  11469  pfxccatin12lem1  11481  swrdccatin2  11482  pfxccatin12lem2  11484  pfxccatin12  11486  swrdccat  11488  swrdccat3blem  11492  swrdccatin2d  11497  pfxccatin12d  11498  cats1lend  11520  cats2catd  11522  s2eqd  11523  s3eqd  11524  s4eqd  11525  s5eqd  11526  s6eqd  11527  s7eqd  11528  s8eqd  11529  crre  11603  replim  11605  remullem  11617  remul2  11619  immul2  11626  cjcj  11629  cjadd  11630  ipcnval  11632  cjmulval  11634  cjneg  11636  imval2  11640  cjreim  11650  cvg1nlemcau  11731  cvg1nlemres  11732  resqrexlemp1rp  11753  resqrexlemfp1  11756  resqrexlemcalc1  11761  resqrexlemcalc2  11762  resqrex  11773  sqabsadd  11802  sqabssub  11803  absreimsq  11814  recan  11856  amgm2  11865  maxabslemab  11953  maxabslemval  11955  max0addsup  11966  minabs  11983  bdtrilem  11986  bdtri  11987  xrmaxadd  12008  xrminadd  12022  xrbdtri  12023  subcn2  12058  reccn2ap  12060  climle  12081  climcvg1nlem  12096  serf0  12099  fsumadd  12154  fsumsplit  12155  sumpr  12161  sumtp  12162  isumadd  12179  sumsplitdc  12180  fsum2dlemstep  12182  fsumshftm  12193  fisumrev2  12194  fsumconst  12202  modfsummodlemstep  12205  telfsumo  12214  fsumparts  12218  binomlem  12231  binom  12232  binom1dif  12235  bcxmaslem1  12236  isumsplit  12239  isumnn0nn  12241  arisum  12246  arisum2  12247  trireciplem  12248  trirecip  12249  geosergap  12254  geo2sum  12262  geo2sum2  12263  cvgratnnlemsumlt  12276  mertenslemi1  12283  mertensabs  12285  fprodmul  12339  fprodsplitdc  12344  fprodabs  12364  fprod2dlemstep  12370  fproddivapf  12379  eftabs  12404  eftvalcn  12405  efcllemp  12406  ege2le3  12419  efcj  12421  efaddlem  12422  efsep  12439  ef4p  12442  efgt1p2  12443  efgt1p  12444  sinval  12450  cosval  12451  tanvalap  12456  tanval2ap  12461  tanval3ap  12462  efi4p  12465  sinneg  12474  cosneg  12475  tannegap  12476  efival  12480  efmival  12481  sinadd  12484  cosadd  12485  tanaddaplem  12486  tanaddap  12487  sinsub  12488  cossub  12489  addsin  12490  subsin  12491  sinmul  12492  cosmul  12493  addcos  12494  subcos  12495  sincossq  12496  cos2t  12498  sin01bnd  12505  cos01bnd  12506  efieq1re  12520  demoivreALT  12522  dvds2ln  12572  odd2np1lem  12620  bitsinv1lem  12709  gcdaddm  12742  bezoutlemnewy  12754  dfgcd3  12768  dvdsgcd  12770  mulgcd  12774  mulgcdr  12776  gcddiv  12777  sqgcd  12787  lcmgcdlem  12836  lcmgcd  12837  qredeu  12856  divgcdcoprm0  12860  cncongr1  12862  oddpwdclemdc  12932  sqrt2irraplemnn  12938  qnumdenbi  12951  zgcdsq  12960  hashdvds  12980  phiprmpw  12981  phimullem  12984  eulerthlema  12989  prmdiv  12994  modprm0  13014  coprimeprodsq  13017  pythagtriplem1  13025  pythagtriplem12  13035  pythagtriplem14  13037  pythagtriplem15  13038  pythagtriplem16  13039  pythagtriplem17  13040  pythagtriplem19  13042  pcval  13056  pcmul  13061  pcdiv  13062  pcqmul  13063  pcid  13084  pcaddlem  13099  pcmpt  13103  pcmpt2  13104  pcmptdvds  13105  pcbc  13111  4sqlem4  13152  mul4sqlem  13153  mul4sq  13154  4sqlem11  13161  4sqlem12  13162  4sqlem15  13165  4sqlem17  13167  ballotfilemfval  13210  ballotfilemfp1  13212  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemfmpn  13215  ballotfilemgval  13248  ballotfilemgun  13249  ballotfilemfrc  13251  ballotfilemfrceq  13253  ennnfonelemp1  13278  nninfdclemp1  13322  ressvalsets  13398  topnvalg  13585  topnpropgd  13587  qusval  13624  qusex  13626  qusaddvallemg  13634  imasmnd2  13739  ismhm  13748  mhmf1o  13757  0mhm  13773  mhmco  13777  mhmeql  13779  isgrpid2  13825  grpnpcan  13877  imasgrp2  13893  mhmmnd  13899  mulgnndir  13934  mulgdir  13937  isnsg3  13990  isghm  14026  ghmnsgima  14051  ghmf1o  14058  conjghm  14059  qusghm  14065  ablsub4  14097  ghmcmn  14111  invghm  14113  gzsumconst  14123  gzsumgsum  14135  gsump1  14137  gsumzfi  14138  gsummptfidmadd  14141  gsumconstcmn  14146  prdsex  14152  prdsval  14153  xpsval  14181  pwsval  14184  mgpvalg  14200  mgptopng  14206  mgpress  14208  rngdi  14217  rngdir  14218  rngpropd  14232  imasrng  14233  srglmhm  14274  srgrmhm  14275  ringo2times  14309  ringcom  14312  ringpropd  14319  ring1  14340  ringlghm  14342  ringrghm  14343  imasring  14345  opprvalg  14350  opprrng  14358  opprring  14360  invrfvald  14405  dvrvald  14417  dvrdir  14426  rdivmuldivd  14427  islmod  14603  lmodlema  14604  islmodd  14605  lmodcom  14645  lmodnegadd  14648  lmodprop2d  14660  rmodislmod  14663  lsssn0  14682  sraval  14749  qusrhm  14840  gsumfsum  14898  expghmap  14917  mulgghm2  14918  mulgrhm  14919  zlmval  14937  znval  14946  psrval  14976  mplvalcoe  15007  cnfval  15221  cnpfval  15222  ispsmet  15350  psmet0  15354  psmettri2  15355  psmetres2  15360  ismet  15371  isxmet  15372  xmettri2  15388  xmetres2  15406  xblss2  15432  xmstri2  15497  mstri2  15498  xmstri  15499  mstri  15500  xmstri3  15501  mstri3  15502  msrtri  15503  comet  15526  bdxmet  15528  txmetcnp  15545  metcnpd  15547  cnmet  15557  ioo2bl  15578  mpomulcn  15593  fsumcncntop  15594  elcncf  15600  mulc1cncf  15616  cncfco  15618  cncfcncntop  15620  cncfmptc  15623  cncfmptid  15624  addccncf  15627  cdivcncfap  15631  negcncf  15632  mulcncflem  15634  limccnp2cntop  15704  reldvg  15706  dvfvalap  15708  eldvap  15709  dvconst  15721  dvconstre  15723  dvconstss  15725  dvaddxxbr  15728  dvmulxxbr  15729  dvcoapbr  15734  dvcjbr  15735  dvexp  15738  dvrecap  15740  dvmptid  15743  dvmptc  15744  dveflem  15753  dvef  15754  elplyd  15768  ply1termlem  15769  plyaddlem1  15774  plymullem1  15775  plyadd  15778  plymul  15779  plycoeid3  15784  plycolemc  15785  plyco  15786  plycjlemc  15787  plycj  15788  plyrecj  15790  dvply1  15792  dvply2g  15793  sinperlem  15835  sinmpi  15842  cosmpi  15843  sinppi  15844  cosppi  15845  efimpi  15846  sinhalfpip  15847  sinhalfpim  15848  coshalfpip  15849  coshalfpim  15850  ptolemy  15851  tangtx  15865  logdivlti  15908  rpcxpadd  15933  rpmulcxp  15937  rplogbchbase  15978  rprelogbmul  15983  binom4  16007  pellexlem2  16009  pellexlem3  16010  wilthlem1  16011  1sgmprm  16025  1sgm2ppw  16026  sgmmul  16027  mersenne  16028  perfect1  16029  perfectlem2  16031  perfect  16032  lgsval  16040  lgsfvalg  16041  lgsval2lem  16046  lgsval4a  16058  lgsneg  16060  lgsdilem  16063  lgsdirprm  16070  lgsdir  16071  lgsdilem2  16072  lgsdi  16073  lgsne0  16074  gausslemma2dlem4  16100  gausslemma2dlem6  16103  lgseisenlem2  16107  lgsquadlem1  16113  lgsquadlem2  16114  lgsquadlem3  16115  lgsquad2lem1  16117  lgsquad2lem2  16118  2lgslem3a  16129  2lgslem3b  16130  2lgslem3c  16131  2lgslem3d  16132  2sqlem2  16151  2sqlem3  16153  2sqlem4  16154  2sqlem8  16159  vtxdgfval  16446  vtxdgfifival  16449  vtxdgop  16450  vtxdgfi0e  16453  vtxdeqd  16454  vtxdfifiun  16455  vtxduspgrfvedgfi  16459  1loopgrvd2fi  16463  repiecele0  16983  repiecege0  16984  repiecef  16985  cvgcmp2nlemabs  16989  trilpolemclim  16993  trilpolemcl  16994  trilpolemisumle  16995  trilpolemeq1  16997  trilpolemlt1  16998  trilpo  17000  redcwlpo  17013  nconstwlpolemgt0  17022  nconstwlpo  17024  neapmkv  17026