Theorem oveq12d 6036

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	⊢ (𝜑 → 𝐴 = 𝐵)
oveq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
oveq12d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		oveq12 6027	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq123d  6039  ovmpodxf  6147  ovmpodf  6153  caovdig  6197  caovdir2d  6199  caovdirg  6200  caovdilemd  6214  caovlem2d  6215  offval  6243  ofvalg  6245  offval2  6251  ofco  6254  caofinvl  6261  offres  6297  nnmsucr  6656  nndir  6658  ecovdi  6815  ecovidi  6816  dfplpq2  7574  dfmpq2  7575  addcmpblnq  7587  mulpipqqs  7593  addassnqg  7602  distrnqg  7607  ltaddnq  7627  halfnqq  7630  enq0tr  7654  addcmpblnq0  7663  addnq0mo  7667  addnnnq0  7669  nqnq0a  7674  distrnq0  7679  addassnq0  7682  distnq0r  7683  nq02m  7685  ltexpri  7833  cauappcvgprlemm  7865  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemmu  7915  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  caucvgprprlem2  7930  mulcmpblnrlemg  7960  mulsrmo  7964  mulsrpr  7966  mulcomsrg  7977  distrsrg  7979  recexgt0sr  7993  mulgt0sr  7998  mulextsr1lem  8000  caucvgsrlemgt1  8015  caucvgsr  8022  addcnsr  8054  mulcnsr  8055  recidpirqlemcalc  8077  axaddcl  8084  axmulcl  8086  axmulcom  8091  axmulass  8093  axdistr  8094  axcaucvglemcau  8118  axcaucvglemres  8119  adddir  8170  muladd11  8312  1p1times  8313  muladd11r  8335  pnpcan2  8419  muladd  8563  subdir  8565  mulsub  8580  mulreim  8784  apadd1  8788  mulext1  8792  recextlem1  8831  muleqadd  8848  divdirap  8877  divadddivap  8907  conjmulap  8909  divcanap5rd  8998  subrecap  9019  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  cnref1o  9885  xnegid  10094  xposdif  10117  xleaddadd  10122  icoshftf1o  10226  lincmb01cmp  10238  iccf1o  10239  fz01en  10288  fzrev3  10322  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzoaddel2  10436  fzosubel  10440  fzosubel2  10441  fzocatel  10445  modqsubdir  10656  addmodlteq  10661  frecuzrdgsuc  10677  frecfzen2  10690  iseqovex  10721  seqvalcd  10724  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seqf1oglem2  10783  seq3id3  10787  seqfeq3  10792  seq3distr  10795  ser3le  10800  mulexp  10841  mulexpzap  10842  expaddzap  10846  expubnd  10859  subsq  10909  binom2  10914  binom21  10915  binom2sub  10916  binom2sub1  10917  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  nn0opthd  10985  facp1  10993  facubnd  11008  bcval  11012  bcn1  11021  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcn2  11027  bcpasc  11029  hashun  11069  hashfz  11086  hashtpgim  11110  ccatlid  11187  ccatass  11189  ccat1st1st  11222  swrdval  11233  swrdspsleq  11252  ccatswrd  11255  pfxval  11259  addlenpfx  11276  ccatpfx  11286  ccatopth  11301  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat  11320  swrdccat3blem  11324  swrdccatin2d  11329  pfxccatin12d  11330  cats1lend  11352  cats2catd  11354  s2eqd  11355  s3eqd  11356  s4eqd  11357  s5eqd  11358  s6eqd  11359  s7eqd  11360  s8eqd  11361  crre  11422  replim  11424  remullem  11436  remul2  11438  immul2  11445  cjcj  11448  cjadd  11449  ipcnval  11451  cjmulval  11453  cjneg  11455  imval2  11459  cjreim  11468  cvg1nlemcau  11549  cvg1nlemres  11550  resqrexlemp1rp  11571  resqrexlemfp1  11574  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrex  11591  sqabsadd  11620  sqabssub  11621  absreimsq  11632  recan  11674  amgm2  11683  maxabslemab  11771  maxabslemval  11773  max0addsup  11784  minabs  11801  bdtrilem  11804  bdtri  11805  xrmaxadd  11826  xrminadd  11840  xrbdtri  11841  subcn2  11876  reccn2ap  11878  climle  11899  climcvg1nlem  11914  serf0  11917  fsumadd  11972  fsumsplit  11973  sumpr  11979  sumtp  11980  isumadd  11997  sumsplitdc  11998  fsum2dlemstep  12000  fsumshftm  12011  fisumrev2  12012  fsumconst  12020  modfsummodlemstep  12023  telfsumo  12032  fsumparts  12036  binomlem  12049  binom  12050  binom1dif  12053  bcxmaslem1  12054  isumsplit  12057  isumnn0nn  12059  arisum  12064  arisum2  12065  trireciplem  12066  trirecip  12067  geosergap  12072  geo2sum  12080  geo2sum2  12081  cvgratnnlemsumlt  12094  mertenslemi1  12101  mertensabs  12103  fprodmul  12157  fprodsplitdc  12162  fprodabs  12182  fprod2dlemstep  12188  fproddivapf  12197  eftabs  12222  eftvalcn  12223  efcllemp  12224  ege2le3  12237  efcj  12239  efaddlem  12240  efsep  12257  ef4p  12260  efgt1p2  12261  efgt1p  12262  sinval  12268  cosval  12269  tanvalap  12274  tanval2ap  12279  tanval3ap  12280  efi4p  12283  sinneg  12292  cosneg  12293  tannegap  12294  efival  12298  efmival  12299  sinadd  12302  cosadd  12303  tanaddaplem  12304  tanaddap  12305  sinsub  12306  cossub  12307  addsin  12308  subsin  12309  sinmul  12310  cosmul  12311  addcos  12312  subcos  12313  sincossq  12314  cos2t  12316  sin01bnd  12323  cos01bnd  12324  efieq1re  12338  demoivreALT  12340  dvds2ln  12390  odd2np1lem  12438  bitsinv1lem  12527  gcdaddm  12560  bezoutlemnewy  12572  dfgcd3  12586  dvdsgcd  12588  mulgcd  12592  mulgcdr  12594  gcddiv  12595  sqgcd  12605  lcmgcdlem  12654  lcmgcd  12655  qredeu  12674  divgcdcoprm0  12678  cncongr1  12680  oddpwdclemdc  12750  sqrt2irraplemnn  12756  qnumdenbi  12769  zgcdsq  12778  hashdvds  12798  phiprmpw  12799  phimullem  12802  eulerthlema  12807  prmdiv  12812  modprm0  12832  coprimeprodsq  12835  pythagtriplem1  12843  pythagtriplem12  12853  pythagtriplem14  12855  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem17  12858  pythagtriplem19  12860  pcval  12874  pcmul  12879  pcdiv  12880  pcqmul  12881  pcid  12902  pcaddlem  12917  pcmpt  12921  pcmpt2  12922  pcmptdvds  12923  pcbc  12929  4sqlem4  12970  mul4sqlem  12971  mul4sq  12972  4sqlem11  12979  4sqlem12  12980  4sqlem15  12983  4sqlem17  12985  ennnfonelemp1  13032  nninfdclemp1  13076  ressvalsets  13152  topnvalg  13339  topnpropgd  13341  prdsex  13357  prdsval  13361  pwsval  13379  qusval  13411  qusex  13413  qusaddvallemg  13421  xpsval  13440  gsumprval  13487  imasmnd2  13540  ismhm  13549  mhmf1o  13558  0mhm  13574  mhmco  13578  mhmeql  13580  gsumfzz  13583  isgrpid2  13628  grpnpcan  13680  imasgrp2  13702  mhmmnd  13708  mulgnndir  13743  mulgdir  13746  isnsg3  13799  isghm  13835  ghmnsgima  13860  ghmf1o  13867  conjghm  13868  qusghm  13874  ablsub4  13905  ghmcmn  13919  invghm  13921  gsumfzmptfidmadd  13931  gsumfzconst  13933  mgpvalg  13942  mgptopng  13948  mgpress  13950  rngdi  13959  rngdir  13960  rngpropd  13974  imasrng  13975  srglmhm  14012  srgrmhm  14013  ringo2times  14047  ringcom  14050  ringpropd  14057  ring1  14078  ringlghm  14080  ringrghm  14081  imasring  14083  opprvalg  14088  opprrng  14096  opprring  14098  invrfvald  14142  dvrvald  14154  dvrdir  14163  rdivmuldivd  14164  islmod  14311  lmodlema  14312  islmodd  14313  lmodcom  14353  lmodnegadd  14356  lmodprop2d  14368  rmodislmod  14371  lsssn0  14390  sraval  14457  qusrhm  14548  gsumfzfsumlemm  14607  expghmap  14627  mulgghm2  14628  mulgrhm  14629  zlmval  14647  znval  14656  psrval  14686  mplvalcoe  14710  cnfval  14924  cnpfval  14925  ispsmet  15053  psmet0  15057  psmettri2  15058  psmetres2  15063  ismet  15074  isxmet  15075  xmettri2  15091  xmetres2  15109  xblss2  15135  xmstri2  15200  mstri2  15201  xmstri  15202  mstri  15203  xmstri3  15204  mstri3  15205  msrtri  15206  comet  15229  bdxmet  15231  txmetcnp  15248  metcnpd  15250  cnmet  15260  ioo2bl  15281  mpomulcn  15296  fsumcncntop  15297  elcncf  15303  mulc1cncf  15319  cncfco  15321  cncfcncntop  15323  cncfmptc  15326  cncfmptid  15327  addccncf  15330  cdivcncfap  15334  negcncf  15335  mulcncflem  15337  limccnp2cntop  15407  reldvg  15409  dvfvalap  15411  eldvap  15412  dvconst  15424  dvconstre  15426  dvconstss  15428  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvcjbr  15438  dvexp  15441  dvrecap  15443  dvmptid  15446  dvmptc  15447  dveflem  15456  dvef  15457  elplyd  15471  ply1termlem  15472  plyaddlem1  15477  plymullem1  15478  plyadd  15481  plymul  15482  plycoeid3  15487  plycolemc  15488  plyco  15489  plycjlemc  15490  plycj  15491  plyrecj  15493  dvply1  15495  dvply2g  15496  sinperlem  15538  sinmpi  15545  cosmpi  15546  sinppi  15547  cosppi  15548  efimpi  15549  sinhalfpip  15550  sinhalfpim  15551  coshalfpip  15552  coshalfpim  15553  ptolemy  15554  tangtx  15568  logdivlti  15611  rpcxpadd  15635  rpmulcxp  15639  rplogbchbase  15680  rprelogbmul  15685  binom4  15709  wilthlem1  15710  1sgmprm  15724  1sgm2ppw  15725  sgmmul  15726  mersenne  15727  perfect1  15728  perfectlem2  15730  perfect  15731  lgsval  15739  lgsfvalg  15740  lgsval2lem  15745  lgsval4a  15757  lgsneg  15759  lgsdilem  15762  lgsdirprm  15769  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  gausslemma2dlem4  15799  gausslemma2dlem6  15802  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  lgsquad2lem2  15817  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2sqlem2  15850  2sqlem3  15852  2sqlem4  15853  2sqlem8  15858  vtxdgfval  16145  vtxdgfifival  16148  vtxdgop  16149  vtxdgfi0e  16152  vtxdeqd  16153  vtxdfifiun  16154  vtxduspgrfvedgfi  16158  1loopgrvd2fi  16162  cvgcmp2nlemabs  16662  trilpolemclim  16666  trilpolemcl  16667  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  trilpo  16673  redcwlpo  16686  nconstwlpolemgt0  16695  nconstwlpo  16697  neapmkv  16699  gsumgfsum  16711  gfsump1  16713