Theorem oveq12d 6025

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

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  oveq123d  6028  ovmpodxf  6136  ovmpodf  6142  caovdig  6186  caovdir2d  6188  caovdirg  6189  caovdilemd  6203  caovlem2d  6204  offval  6232  ofvalg  6234  offval2  6240  ofco  6243  caofinvl  6250  offres  6286  nnmsucr  6642  nndir  6644  ecovdi  6801  ecovidi  6802  dfplpq2  7552  dfmpq2  7553  addcmpblnq  7565  mulpipqqs  7571  addassnqg  7580  distrnqg  7585  ltaddnq  7605  halfnqq  7608  enq0tr  7632  addcmpblnq0  7641  addnq0mo  7645  addnnnq0  7647  nqnq0a  7652  distrnq0  7657  addassnq0  7660  distnq0r  7661  nq02m  7663  ltexpri  7811  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemmu  7893  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem2  7908  mulcmpblnrlemg  7938  mulsrmo  7942  mulsrpr  7944  mulcomsrg  7955  distrsrg  7957  recexgt0sr  7971  mulgt0sr  7976  mulextsr1lem  7978  caucvgsrlemgt1  7993  caucvgsr  8000  addcnsr  8032  mulcnsr  8033  recidpirqlemcalc  8055  axaddcl  8062  axmulcl  8064  axmulcom  8069  axmulass  8071  axdistr  8072  axcaucvglemcau  8096  axcaucvglemres  8097  adddir  8148  muladd11  8290  1p1times  8291  muladd11r  8313  pnpcan2  8397  muladd  8541  subdir  8543  mulsub  8558  mulreim  8762  apadd1  8766  mulext1  8770  recextlem1  8809  muleqadd  8826  divdirap  8855  divadddivap  8885  conjmulap  8887  divcanap5rd  8976  subrecap  8997  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  cnref1o  9858  xnegid  10067  xposdif  10090  xleaddadd  10095  icoshftf1o  10199  lincmb01cmp  10211  iccf1o  10212  fz01en  10261  fzrev3  10295  fzrevral2  10314  fzrevral3  10315  fzshftral  10316  fzoaddel2  10408  fzosubel  10412  fzosubel2  10413  fzocatel  10417  modqsubdir  10627  addmodlteq  10632  frecuzrdgsuc  10648  frecfzen2  10661  iseqovex  10692  seqvalcd  10695  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seqf1oglem2  10754  seq3id3  10758  seqfeq3  10763  seq3distr  10766  ser3le  10771  mulexp  10812  mulexpzap  10813  expaddzap  10817  expubnd  10830  subsq  10880  binom2  10885  binom21  10886  binom2sub  10887  binom2sub1  10888  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  nn0opthd  10956  facp1  10964  facubnd  10979  bcval  10983  bcn1  10992  bcm1k  10994  bcp1n  10995  bcp1nk  10996  bcval5  10997  bcn2  10998  bcpasc  11000  hashun  11039  hashfz  11056  ccatlid  11154  ccatass  11156  ccat1st1st  11187  swrdval  11195  swrdspsleq  11214  ccatswrd  11217  pfxval  11221  addlenpfx  11238  ccatpfx  11248  ccatopth  11263  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccat  11282  swrdccat3blem  11286  swrdccatin2d  11291  pfxccatin12d  11292  cats1lend  11314  cats2catd  11316  s2eqd  11317  s3eqd  11318  s4eqd  11319  s5eqd  11320  s6eqd  11321  s7eqd  11322  s8eqd  11323  crre  11383  replim  11385  remullem  11397  remul2  11399  immul2  11406  cjcj  11409  cjadd  11410  ipcnval  11412  cjmulval  11414  cjneg  11416  imval2  11420  cjreim  11429  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemp1rp  11532  resqrexlemfp1  11535  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrex  11552  sqabsadd  11581  sqabssub  11582  absreimsq  11593  recan  11635  amgm2  11644  maxabslemab  11732  maxabslemval  11734  max0addsup  11745  minabs  11762  bdtrilem  11765  bdtri  11766  xrmaxadd  11787  xrminadd  11801  xrbdtri  11802  subcn2  11837  reccn2ap  11839  climle  11860  climcvg1nlem  11875  serf0  11878  fsumadd  11932  fsumsplit  11933  sumpr  11939  sumtp  11940  isumadd  11957  sumsplitdc  11958  fsum2dlemstep  11960  fsumshftm  11971  fisumrev2  11972  fsumconst  11980  modfsummodlemstep  11983  telfsumo  11992  fsumparts  11996  binomlem  12009  binom  12010  binom1dif  12013  bcxmaslem1  12014  isumsplit  12017  isumnn0nn  12019  arisum  12024  arisum2  12025  trireciplem  12026  trirecip  12027  geosergap  12032  geo2sum  12040  geo2sum2  12041  cvgratnnlemsumlt  12054  mertenslemi1  12061  mertensabs  12063  fprodmul  12117  fprodsplitdc  12122  fprodabs  12142  fprod2dlemstep  12148  fproddivapf  12157  eftabs  12182  eftvalcn  12183  efcllemp  12184  ege2le3  12197  efcj  12199  efaddlem  12200  efsep  12217  ef4p  12220  efgt1p2  12221  efgt1p  12222  sinval  12228  cosval  12229  tanvalap  12234  tanval2ap  12239  tanval3ap  12240  efi4p  12243  sinneg  12252  cosneg  12253  tannegap  12254  efival  12258  efmival  12259  sinadd  12262  cosadd  12263  tanaddaplem  12264  tanaddap  12265  sinsub  12266  cossub  12267  addsin  12268  subsin  12269  sinmul  12270  cosmul  12271  addcos  12272  subcos  12273  sincossq  12274  cos2t  12276  sin01bnd  12283  cos01bnd  12284  efieq1re  12298  demoivreALT  12300  dvds2ln  12350  odd2np1lem  12398  bitsinv1lem  12487  gcdaddm  12520  bezoutlemnewy  12532  dfgcd3  12546  dvdsgcd  12548  mulgcd  12552  mulgcdr  12554  gcddiv  12555  sqgcd  12565  lcmgcdlem  12614  lcmgcd  12615  qredeu  12634  divgcdcoprm0  12638  cncongr1  12640  oddpwdclemdc  12710  sqrt2irraplemnn  12716  qnumdenbi  12729  zgcdsq  12738  hashdvds  12758  phiprmpw  12759  phimullem  12762  eulerthlema  12767  prmdiv  12772  modprm0  12792  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem15  12816  pythagtriplem16  12817  pythagtriplem17  12818  pythagtriplem19  12820  pcval  12834  pcmul  12839  pcdiv  12840  pcqmul  12841  pcid  12862  pcaddlem  12877  pcmpt  12881  pcmpt2  12882  pcmptdvds  12883  pcbc  12889  4sqlem4  12930  mul4sqlem  12931  mul4sq  12932  4sqlem11  12939  4sqlem12  12940  4sqlem15  12943  4sqlem17  12945  ennnfonelemp1  12992  nninfdclemp1  13036  ressvalsets  13112  topnvalg  13299  topnpropgd  13301  prdsex  13317  prdsval  13321  pwsval  13339  qusval  13371  qusex  13373  qusaddvallemg  13381  xpsval  13400  gsumprval  13447  imasmnd2  13500  ismhm  13509  mhmf1o  13518  0mhm  13534  mhmco  13538  mhmeql  13540  gsumfzz  13543  isgrpid2  13588  grpnpcan  13640  imasgrp2  13662  mhmmnd  13668  mulgnndir  13703  mulgdir  13706  isnsg3  13759  isghm  13795  ghmnsgima  13820  ghmf1o  13827  conjghm  13828  qusghm  13834  ablsub4  13865  ghmcmn  13879  invghm  13881  gsumfzmptfidmadd  13891  gsumfzconst  13893  mgpvalg  13901  mgptopng  13907  mgpress  13909  rngdi  13918  rngdir  13919  rngpropd  13933  imasrng  13934  srglmhm  13971  srgrmhm  13972  ringo2times  14006  ringcom  14009  ringpropd  14016  ring1  14037  ringlghm  14039  ringrghm  14040  imasring  14042  opprvalg  14047  opprrng  14055  opprring  14057  invrfvald  14101  dvrvald  14113  dvrdir  14122  rdivmuldivd  14123  islmod  14270  lmodlema  14271  islmodd  14272  lmodcom  14312  lmodnegadd  14315  lmodprop2d  14327  rmodislmod  14330  lsssn0  14349  sraval  14416  qusrhm  14507  gsumfzfsumlemm  14566  expghmap  14586  mulgghm2  14587  mulgrhm  14588  zlmval  14606  znval  14615  psrval  14645  mplvalcoe  14669  cnfval  14883  cnpfval  14884  ispsmet  15012  psmet0  15016  psmettri2  15017  psmetres2  15022  ismet  15033  isxmet  15034  xmettri2  15050  xmetres2  15068  xblss2  15094  xmstri2  15159  mstri2  15160  xmstri  15161  mstri  15162  xmstri3  15163  mstri3  15164  msrtri  15165  comet  15188  bdxmet  15190  txmetcnp  15207  metcnpd  15209  cnmet  15219  ioo2bl  15240  mpomulcn  15255  fsumcncntop  15256  elcncf  15262  mulc1cncf  15278  cncfco  15280  cncfcncntop  15282  cncfmptc  15285  cncfmptid  15286  addccncf  15289  cdivcncfap  15293  negcncf  15294  mulcncflem  15296  limccnp2cntop  15366  reldvg  15368  dvfvalap  15370  eldvap  15371  dvconst  15383  dvconstre  15385  dvconstss  15387  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvexp  15400  dvrecap  15402  dvmptid  15405  dvmptc  15406  dveflem  15415  dvef  15416  elplyd  15430  ply1termlem  15431  plyaddlem1  15436  plymullem1  15437  plyadd  15440  plymul  15441  plycoeid3  15446  plycolemc  15447  plyco  15448  plycjlemc  15449  plycj  15450  plyrecj  15452  dvply1  15454  dvply2g  15455  sinperlem  15497  sinmpi  15504  cosmpi  15505  sinppi  15506  cosppi  15507  efimpi  15508  sinhalfpip  15509  sinhalfpim  15510  coshalfpip  15511  coshalfpim  15512  ptolemy  15513  tangtx  15527  logdivlti  15570  rpcxpadd  15594  rpmulcxp  15598  rplogbchbase  15639  rprelogbmul  15644  binom4  15668  wilthlem1  15669  1sgmprm  15683  1sgm2ppw  15684  sgmmul  15685  mersenne  15686  perfect1  15687  perfectlem2  15689  perfect  15690  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsval4a  15716  lgsneg  15718  lgsdilem  15721  lgsdirprm  15728  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  gausslemma2dlem4  15758  gausslemma2dlem6  15761  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad2lem2  15776  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2sqlem2  15809  2sqlem3  15811  2sqlem4  15812  2sqlem8  15817  vtxdgfval  16047  vtxdgfifival  16050  vtxdgop  16051  vtxdgfi0e  16054  vtxdeqd  16055  vtxdfifiun  16056  cvgcmp2nlemabs  16460  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trilpo  16471  redcwlpo  16483  nconstwlpolemgt0  16492  nconstwlpo  16494  neapmkv  16496