Theorem oveq12d 6031

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 6022	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq123d  6034  ovmpodxf  6142  ovmpodf  6148  caovdig  6192  caovdir2d  6194  caovdirg  6195  caovdilemd  6209  caovlem2d  6210  offval  6238  ofvalg  6240  offval2  6246  ofco  6249  caofinvl  6256  offres  6292  nnmsucr  6651  nndir  6653  ecovdi  6810  ecovidi  6811  dfplpq2  7564  dfmpq2  7565  addcmpblnq  7577  mulpipqqs  7583  addassnqg  7592  distrnqg  7597  ltaddnq  7617  halfnqq  7620  enq0tr  7644  addcmpblnq0  7653  addnq0mo  7657  addnnnq0  7659  nqnq0a  7664  distrnq0  7669  addassnq0  7672  distnq0r  7673  nq02m  7675  ltexpri  7823  cauappcvgprlemm  7855  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemmu  7905  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem2  7920  mulcmpblnrlemg  7950  mulsrmo  7954  mulsrpr  7956  mulcomsrg  7967  distrsrg  7969  recexgt0sr  7983  mulgt0sr  7988  mulextsr1lem  7990  caucvgsrlemgt1  8005  caucvgsr  8012  addcnsr  8044  mulcnsr  8045  recidpirqlemcalc  8067  axaddcl  8074  axmulcl  8076  axmulcom  8081  axmulass  8083  axdistr  8084  axcaucvglemcau  8108  axcaucvglemres  8109  adddir  8160  muladd11  8302  1p1times  8303  muladd11r  8325  pnpcan2  8409  muladd  8553  subdir  8555  mulsub  8570  mulreim  8774  apadd1  8778  mulext1  8782  recextlem1  8821  muleqadd  8838  divdirap  8867  divadddivap  8897  conjmulap  8899  divcanap5rd  8988  subrecap  9009  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  cnref1o  9875  xnegid  10084  xposdif  10107  xleaddadd  10112  icoshftf1o  10216  lincmb01cmp  10228  iccf1o  10229  fz01en  10278  fzrev3  10312  fzrevral2  10331  fzrevral3  10332  fzshftral  10333  fzoaddel2  10425  fzosubel  10429  fzosubel2  10430  fzocatel  10434  modqsubdir  10645  addmodlteq  10650  frecuzrdgsuc  10666  frecfzen2  10679  iseqovex  10710  seqvalcd  10713  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seqf1oglem2  10772  seq3id3  10776  seqfeq3  10781  seq3distr  10784  ser3le  10789  mulexp  10830  mulexpzap  10831  expaddzap  10835  expubnd  10848  subsq  10898  binom2  10903  binom21  10904  binom2sub  10905  binom2sub1  10906  binom3  10909  sqoddm1div8  10945  mulsubdivbinom2ap  10963  nn0opthlem1d  10972  nn0opthd  10974  facp1  10982  facubnd  10997  bcval  11001  bcn1  11010  bcm1k  11012  bcp1n  11013  bcp1nk  11014  bcval5  11015  bcn2  11016  bcpasc  11018  hashun  11058  hashfz  11075  ccatlid  11173  ccatass  11175  ccat1st1st  11208  swrdval  11219  swrdspsleq  11238  ccatswrd  11241  pfxval  11245  addlenpfx  11262  ccatpfx  11272  ccatopth  11287  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccat  11306  swrdccat3blem  11310  swrdccatin2d  11315  pfxccatin12d  11316  cats1lend  11338  cats2catd  11340  s2eqd  11341  s3eqd  11342  s4eqd  11343  s5eqd  11344  s6eqd  11345  s7eqd  11346  s8eqd  11347  crre  11408  replim  11410  remullem  11422  remul2  11424  immul2  11431  cjcj  11434  cjadd  11435  ipcnval  11437  cjmulval  11439  cjneg  11441  imval2  11445  cjreim  11454  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemp1rp  11557  resqrexlemfp1  11560  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrex  11577  sqabsadd  11606  sqabssub  11607  absreimsq  11618  recan  11660  amgm2  11669  maxabslemab  11757  maxabslemval  11759  max0addsup  11770  minabs  11787  bdtrilem  11790  bdtri  11791  xrmaxadd  11812  xrminadd  11826  xrbdtri  11827  subcn2  11862  reccn2ap  11864  climle  11885  climcvg1nlem  11900  serf0  11903  fsumadd  11957  fsumsplit  11958  sumpr  11964  sumtp  11965  isumadd  11982  sumsplitdc  11983  fsum2dlemstep  11985  fsumshftm  11996  fisumrev2  11997  fsumconst  12005  modfsummodlemstep  12008  telfsumo  12017  fsumparts  12021  binomlem  12034  binom  12035  binom1dif  12038  bcxmaslem1  12039  isumsplit  12042  isumnn0nn  12044  arisum  12049  arisum2  12050  trireciplem  12051  trirecip  12052  geosergap  12057  geo2sum  12065  geo2sum2  12066  cvgratnnlemsumlt  12079  mertenslemi1  12086  mertensabs  12088  fprodmul  12142  fprodsplitdc  12147  fprodabs  12167  fprod2dlemstep  12173  fproddivapf  12182  eftabs  12207  eftvalcn  12208  efcllemp  12209  ege2le3  12222  efcj  12224  efaddlem  12225  efsep  12242  ef4p  12245  efgt1p2  12246  efgt1p  12247  sinval  12253  cosval  12254  tanvalap  12259  tanval2ap  12264  tanval3ap  12265  efi4p  12268  sinneg  12277  cosneg  12278  tannegap  12279  efival  12283  efmival  12284  sinadd  12287  cosadd  12288  tanaddaplem  12289  tanaddap  12290  sinsub  12291  cossub  12292  addsin  12293  subsin  12294  sinmul  12295  cosmul  12296  addcos  12297  subcos  12298  sincossq  12299  cos2t  12301  sin01bnd  12308  cos01bnd  12309  efieq1re  12323  demoivreALT  12325  dvds2ln  12375  odd2np1lem  12423  bitsinv1lem  12512  gcdaddm  12545  bezoutlemnewy  12557  dfgcd3  12571  dvdsgcd  12573  mulgcd  12577  mulgcdr  12579  gcddiv  12580  sqgcd  12590  lcmgcdlem  12639  lcmgcd  12640  qredeu  12659  divgcdcoprm0  12663  cncongr1  12665  oddpwdclemdc  12735  sqrt2irraplemnn  12741  qnumdenbi  12754  zgcdsq  12763  hashdvds  12783  phiprmpw  12784  phimullem  12787  eulerthlema  12792  prmdiv  12797  modprm0  12817  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  pythagtriplem19  12845  pcval  12859  pcmul  12864  pcdiv  12865  pcqmul  12866  pcid  12887  pcaddlem  12902  pcmpt  12906  pcmpt2  12907  pcmptdvds  12908  pcbc  12914  4sqlem4  12955  mul4sqlem  12956  mul4sq  12957  4sqlem11  12964  4sqlem12  12965  4sqlem15  12968  4sqlem17  12970  ennnfonelemp1  13017  nninfdclemp1  13061  ressvalsets  13137  topnvalg  13324  topnpropgd  13326  prdsex  13342  prdsval  13346  pwsval  13364  qusval  13396  qusex  13398  qusaddvallemg  13406  xpsval  13425  gsumprval  13472  imasmnd2  13525  ismhm  13534  mhmf1o  13543  0mhm  13559  mhmco  13563  mhmeql  13565  gsumfzz  13568  isgrpid2  13613  grpnpcan  13665  imasgrp2  13687  mhmmnd  13693  mulgnndir  13728  mulgdir  13731  isnsg3  13784  isghm  13820  ghmnsgima  13845  ghmf1o  13852  conjghm  13853  qusghm  13859  ablsub4  13890  ghmcmn  13904  invghm  13906  gsumfzmptfidmadd  13916  gsumfzconst  13918  mgpvalg  13926  mgptopng  13932  mgpress  13934  rngdi  13943  rngdir  13944  rngpropd  13958  imasrng  13959  srglmhm  13996  srgrmhm  13997  ringo2times  14031  ringcom  14034  ringpropd  14041  ring1  14062  ringlghm  14064  ringrghm  14065  imasring  14067  opprvalg  14072  opprrng  14080  opprring  14082  invrfvald  14126  dvrvald  14138  dvrdir  14147  rdivmuldivd  14148  islmod  14295  lmodlema  14296  islmodd  14297  lmodcom  14337  lmodnegadd  14340  lmodprop2d  14352  rmodislmod  14355  lsssn0  14374  sraval  14441  qusrhm  14532  gsumfzfsumlemm  14591  expghmap  14611  mulgghm2  14612  mulgrhm  14613  zlmval  14631  znval  14640  psrval  14670  mplvalcoe  14694  cnfval  14908  cnpfval  14909  ispsmet  15037  psmet0  15041  psmettri2  15042  psmetres2  15047  ismet  15058  isxmet  15059  xmettri2  15075  xmetres2  15093  xblss2  15119  xmstri2  15184  mstri2  15185  xmstri  15186  mstri  15187  xmstri3  15188  mstri3  15189  msrtri  15190  comet  15213  bdxmet  15215  txmetcnp  15232  metcnpd  15234  cnmet  15244  ioo2bl  15265  mpomulcn  15280  fsumcncntop  15281  elcncf  15287  mulc1cncf  15303  cncfco  15305  cncfcncntop  15307  cncfmptc  15310  cncfmptid  15311  addccncf  15314  cdivcncfap  15318  negcncf  15319  mulcncflem  15321  limccnp2cntop  15391  reldvg  15393  dvfvalap  15395  eldvap  15396  dvconst  15408  dvconstre  15410  dvconstss  15412  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvexp  15425  dvrecap  15427  dvmptid  15430  dvmptc  15431  dveflem  15440  dvef  15441  elplyd  15455  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plyadd  15465  plymul  15466  plycoeid3  15471  plycolemc  15472  plyco  15473  plycjlemc  15474  plycj  15475  plyrecj  15477  dvply1  15479  dvply2g  15480  sinperlem  15522  sinmpi  15529  cosmpi  15530  sinppi  15531  cosppi  15532  efimpi  15533  sinhalfpip  15534  sinhalfpim  15535  coshalfpip  15536  coshalfpim  15537  ptolemy  15538  tangtx  15552  logdivlti  15595  rpcxpadd  15619  rpmulcxp  15623  rplogbchbase  15664  rprelogbmul  15669  binom4  15693  wilthlem1  15694  1sgmprm  15708  1sgm2ppw  15709  sgmmul  15710  mersenne  15711  perfect1  15712  perfectlem2  15714  perfect  15715  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsdilem  15746  lgsdirprm  15753  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem4  15783  gausslemma2dlem6  15786  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad2lem2  15801  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2sqlem2  15834  2sqlem3  15836  2sqlem4  15837  2sqlem8  15842  vtxdgfval  16094  vtxdgfifival  16097  vtxdgop  16098  vtxdgfi0e  16101  vtxdeqd  16102  vtxdfifiun  16103  vtxduspgrfvedgfi  16107  1loopgrvd2fi  16111  cvgcmp2nlemabs  16572  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trilpo  16583  redcwlpo  16595  nconstwlpolemgt0  16604  nconstwlpo  16606  neapmkv  16608