Theorem oveq12d 6046

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 6037	. 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 6028

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveq123d  6049  ovmpodxf  6157  ovmpodf  6163  caovdig  6207  caovdir2d  6209  caovdirg  6210  caovdilemd  6224  caovlem2d  6225  offval  6252  ofvalg  6254  offval2  6260  ofco  6263  caofinvl  6270  offres  6306  nnmsucr  6699  nndir  6701  ecovdi  6858  ecovidi  6859  dfplpq2  7634  dfmpq2  7635  addcmpblnq  7647  mulpipqqs  7653  addassnqg  7662  distrnqg  7667  ltaddnq  7687  halfnqq  7690  enq0tr  7714  addcmpblnq0  7723  addnq0mo  7727  addnnnq0  7729  nqnq0a  7734  distrnq0  7739  addassnq0  7742  distnq0r  7743  nq02m  7745  ltexpri  7893  cauappcvgprlemm  7925  cauappcvgprlemloc  7932  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlem2  7940  cauappcvgprlemlim  7941  cauappcvgpr  7942  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemm  7948  caucvgprlemloc  7955  caucvgprlemcl  7956  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprlem2  7960  caucvgpr  7962  caucvgprprlemelu  7966  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemmu  7975  caucvgprprlemopu  7979  caucvgprprlemloc  7983  caucvgprprlemclphr  7985  caucvgprprlemexbt  7986  caucvgprprlem2  7990  mulcmpblnrlemg  8020  mulsrmo  8024  mulsrpr  8026  mulcomsrg  8037  distrsrg  8039  recexgt0sr  8053  mulgt0sr  8058  mulextsr1lem  8060  caucvgsrlemgt1  8075  caucvgsr  8082  addcnsr  8114  mulcnsr  8115  recidpirqlemcalc  8137  axaddcl  8144  axmulcl  8146  axmulcom  8151  axmulass  8153  axdistr  8154  axcaucvglemcau  8178  axcaucvglemres  8179  adddir  8230  muladd11  8371  1p1times  8372  muladd11r  8394  pnpcan2  8478  muladd  8622  subdir  8624  mulsub  8639  mulreim  8843  apadd1  8847  mulext1  8851  recextlem1  8890  muleqadd  8907  divdirap  8936  divadddivap  8966  conjmulap  8968  divcanap5rd  9057  subrecap  9078  xp1d2m1eqxm1d2  9456  div4p1lem1div2  9457  cnref1o  9946  xnegid  10155  xposdif  10178  xleaddadd  10183  icoshftf1o  10287  lincmb01cmp  10299  iccf1o  10301  fz01en  10350  fzrev3  10384  fzrevral2  10403  fzrevral3  10404  fzshftral  10405  fzoaddel2  10498  fzosubel  10502  fzosubel2  10503  fzocatel  10507  modqsubdir  10718  addmodlteq  10723  frecuzrdgsuc  10739  frecfzen2  10752  iseqovex  10783  seqvalcd  10786  seq3caopr3  10816  seqcaopr3g  10817  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seqf1oglem2  10845  seq3id3  10849  seqfeq3  10854  seq3distr  10857  ser3le  10862  mulexp  10903  mulexpzap  10904  expaddzap  10908  expubnd  10921  subsq  10971  binom2  10976  binom21  10977  binom2sub  10978  binom2sub1  10979  binom3  10982  sqoddm1div8  11018  mulsubdivbinom2ap  11036  nn0opthlem1d  11045  nn0opthd  11047  facp1  11055  facubnd  11070  bcval  11074  bcn1  11083  bcm1k  11085  bcp1n  11086  bcp1nk  11087  bcval5  11088  bcn2  11089  bcpasc  11091  hashun  11131  hashfz  11148  hashtpgim  11172  ccatlid  11249  ccatass  11251  ccat1st1st  11284  swrdval  11295  swrdspsleq  11314  ccatswrd  11317  pfxval  11321  addlenpfx  11338  ccatpfx  11348  ccatopth  11363  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  swrdccat  11382  swrdccat3blem  11386  swrdccatin2d  11391  pfxccatin12d  11392  cats1lend  11414  cats2catd  11416  s2eqd  11417  s3eqd  11418  s4eqd  11419  s5eqd  11420  s6eqd  11421  s7eqd  11422  s8eqd  11423  crre  11497  replim  11499  remullem  11511  remul2  11513  immul2  11520  cjcj  11523  cjadd  11524  ipcnval  11526  cjmulval  11528  cjneg  11530  imval2  11534  cjreim  11543  cvg1nlemcau  11624  cvg1nlemres  11625  resqrexlemp1rp  11646  resqrexlemfp1  11649  resqrexlemcalc1  11654  resqrexlemcalc2  11655  resqrex  11666  sqabsadd  11695  sqabssub  11696  absreimsq  11707  recan  11749  amgm2  11758  maxabslemab  11846  maxabslemval  11848  max0addsup  11859  minabs  11876  bdtrilem  11879  bdtri  11880  xrmaxadd  11901  xrminadd  11915  xrbdtri  11916  subcn2  11951  reccn2ap  11953  climle  11974  climcvg1nlem  11989  serf0  11992  fsumadd  12047  fsumsplit  12048  sumpr  12054  sumtp  12055  isumadd  12072  sumsplitdc  12073  fsum2dlemstep  12075  fsumshftm  12086  fisumrev2  12087  fsumconst  12095  modfsummodlemstep  12098  telfsumo  12107  fsumparts  12111  binomlem  12124  binom  12125  binom1dif  12128  bcxmaslem1  12129  isumsplit  12132  isumnn0nn  12134  arisum  12139  arisum2  12140  trireciplem  12141  trirecip  12142  geosergap  12147  geo2sum  12155  geo2sum2  12156  cvgratnnlemsumlt  12169  mertenslemi1  12176  mertensabs  12178  fprodmul  12232  fprodsplitdc  12237  fprodabs  12257  fprod2dlemstep  12263  fproddivapf  12272  eftabs  12297  eftvalcn  12298  efcllemp  12299  ege2le3  12312  efcj  12314  efaddlem  12315  efsep  12332  ef4p  12335  efgt1p2  12336  efgt1p  12337  sinval  12343  cosval  12344  tanvalap  12349  tanval2ap  12354  tanval3ap  12355  efi4p  12358  sinneg  12367  cosneg  12368  tannegap  12369  efival  12373  efmival  12374  sinadd  12377  cosadd  12378  tanaddaplem  12379  tanaddap  12380  sinsub  12381  cossub  12382  addsin  12383  subsin  12384  sinmul  12385  cosmul  12386  addcos  12387  subcos  12388  sincossq  12389  cos2t  12391  sin01bnd  12398  cos01bnd  12399  efieq1re  12413  demoivreALT  12415  dvds2ln  12465  odd2np1lem  12513  bitsinv1lem  12602  gcdaddm  12635  bezoutlemnewy  12647  dfgcd3  12661  dvdsgcd  12663  mulgcd  12667  mulgcdr  12669  gcddiv  12670  sqgcd  12680  lcmgcdlem  12729  lcmgcd  12730  qredeu  12749  divgcdcoprm0  12753  cncongr1  12755  oddpwdclemdc  12825  sqrt2irraplemnn  12831  qnumdenbi  12844  zgcdsq  12853  hashdvds  12873  phiprmpw  12874  phimullem  12877  eulerthlema  12882  prmdiv  12887  modprm0  12907  coprimeprodsq  12910  pythagtriplem1  12918  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem15  12931  pythagtriplem16  12932  pythagtriplem17  12933  pythagtriplem19  12935  pcval  12949  pcmul  12954  pcdiv  12955  pcqmul  12956  pcid  12977  pcaddlem  12992  pcmpt  12996  pcmpt2  12997  pcmptdvds  12998  pcbc  13004  4sqlem4  13045  mul4sqlem  13046  mul4sq  13047  4sqlem11  13054  4sqlem12  13055  4sqlem15  13058  4sqlem17  13060  ennnfonelemp1  13107  nninfdclemp1  13151  ressvalsets  13227  topnvalg  13414  topnpropgd  13416  prdsex  13432  prdsval  13436  pwsval  13454  qusval  13486  qusex  13488  qusaddvallemg  13496  xpsval  13515  gsumprval  13562  imasmnd2  13615  ismhm  13624  mhmf1o  13633  0mhm  13649  mhmco  13653  mhmeql  13655  gsumfzz  13658  isgrpid2  13703  grpnpcan  13755  imasgrp2  13777  mhmmnd  13783  mulgnndir  13818  mulgdir  13821  isnsg3  13874  isghm  13910  ghmnsgima  13935  ghmf1o  13942  conjghm  13943  qusghm  13949  ablsub4  13980  ghmcmn  13994  invghm  13996  gsumfzmptfidmadd  14006  gsumfzconst  14008  mgpvalg  14017  mgptopng  14023  mgpress  14025  rngdi  14034  rngdir  14035  rngpropd  14049  imasrng  14050  srglmhm  14087  srgrmhm  14088  ringo2times  14122  ringcom  14125  ringpropd  14132  ring1  14153  ringlghm  14155  ringrghm  14156  imasring  14158  opprvalg  14163  opprrng  14171  opprring  14173  invrfvald  14217  dvrvald  14229  dvrdir  14238  rdivmuldivd  14239  islmod  14387  lmodlema  14388  islmodd  14389  lmodcom  14429  lmodnegadd  14432  lmodprop2d  14444  rmodislmod  14447  lsssn0  14466  sraval  14533  qusrhm  14624  gsumfzfsumlemm  14683  expghmap  14703  mulgghm2  14704  mulgrhm  14705  zlmval  14723  znval  14732  psrval  14762  mplvalcoe  14791  cnfval  15005  cnpfval  15006  ispsmet  15134  psmet0  15138  psmettri2  15139  psmetres2  15144  ismet  15155  isxmet  15156  xmettri2  15172  xmetres2  15190  xblss2  15216  xmstri2  15281  mstri2  15282  xmstri  15283  mstri  15284  xmstri3  15285  mstri3  15286  msrtri  15287  comet  15310  bdxmet  15312  txmetcnp  15329  metcnpd  15331  cnmet  15341  ioo2bl  15362  mpomulcn  15377  fsumcncntop  15378  elcncf  15384  mulc1cncf  15400  cncfco  15402  cncfcncntop  15404  cncfmptc  15407  cncfmptid  15408  addccncf  15411  cdivcncfap  15415  negcncf  15416  mulcncflem  15418  limccnp2cntop  15488  reldvg  15490  dvfvalap  15492  eldvap  15493  dvconst  15505  dvconstre  15507  dvconstss  15509  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvexp  15522  dvrecap  15524  dvmptid  15527  dvmptc  15528  dveflem  15537  dvef  15538  elplyd  15552  ply1termlem  15553  plyaddlem1  15558  plymullem1  15559  plyadd  15562  plymul  15563  plycoeid3  15568  plycolemc  15569  plyco  15570  plycjlemc  15571  plycj  15572  plyrecj  15574  dvply1  15576  dvply2g  15577  sinperlem  15619  sinmpi  15626  cosmpi  15627  sinppi  15628  cosppi  15629  efimpi  15630  sinhalfpip  15631  sinhalfpim  15632  coshalfpip  15633  coshalfpim  15634  ptolemy  15635  tangtx  15649  logdivlti  15692  rpcxpadd  15716  rpmulcxp  15720  rplogbchbase  15761  rprelogbmul  15766  binom4  15790  pellexlem2  15792  pellexlem3  15793  wilthlem1  15794  1sgmprm  15808  1sgm2ppw  15809  sgmmul  15810  mersenne  15811  perfect1  15812  perfectlem2  15814  perfect  15815  lgsval  15823  lgsfvalg  15824  lgsval2lem  15829  lgsval4a  15841  lgsneg  15843  lgsdilem  15846  lgsdirprm  15853  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  gausslemma2dlem4  15883  gausslemma2dlem6  15886  lgseisenlem2  15890  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem1  15900  lgsquad2lem2  15901  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2sqlem2  15934  2sqlem3  15936  2sqlem4  15937  2sqlem8  15942  vtxdgfval  16229  vtxdgfifival  16232  vtxdgop  16233  vtxdgfi0e  16236  vtxdeqd  16237  vtxdfifiun  16238  vtxduspgrfvedgfi  16242  1loopgrvd2fi  16246  repiecele0  16758  repiecege0  16759  repiecef  16760  cvgcmp2nlemabs  16764  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  trilpo  16775  redcwlpo  16788  nconstwlpolemgt0  16797  nconstwlpo  16799  neapmkv  16801  gsumgfsum  16813  gfsump1  16815