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

Assertion

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

Proof of Theorem oveq12d

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

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  7617  dfmpq2  7618  addcmpblnq  7630  mulpipqqs  7636  addassnqg  7645  distrnqg  7650  ltaddnq  7670  halfnqq  7673  enq0tr  7697  addcmpblnq0  7706  addnq0mo  7710  addnnnq0  7712  nqnq0a  7717  distrnq0  7722  addassnq0  7725  distnq0r  7726  nq02m  7728  ltexpri  7876  cauappcvgprlemm  7908  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgprlemlim  7924  cauappcvgpr  7925  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemmu  7958  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem2  7973  mulcmpblnrlemg  8003  mulsrmo  8007  mulsrpr  8009  mulcomsrg  8020  distrsrg  8022  recexgt0sr  8036  mulgt0sr  8041  mulextsr1lem  8043  caucvgsrlemgt1  8058  caucvgsr  8065  addcnsr  8097  mulcnsr  8098  recidpirqlemcalc  8120  axaddcl  8127  axmulcl  8129  axmulcom  8134  axmulass  8136  axdistr  8137  axcaucvglemcau  8161  axcaucvglemres  8162  adddir  8213  muladd11  8354  1p1times  8355  muladd11r  8377  pnpcan2  8461  muladd  8605  subdir  8607  mulsub  8622  mulreim  8826  apadd1  8830  mulext1  8834  recextlem1  8873  muleqadd  8890  divdirap  8919  divadddivap  8949  conjmulap  8951  divcanap5rd  9040  subrecap  9061  xp1d2m1eqxm1d2  9439  div4p1lem1div2  9440  cnref1o  9929  xnegid  10138  xposdif  10161  xleaddadd  10166  icoshftf1o  10270  lincmb01cmp  10282  iccf1o  10284  fz01en  10333  fzrev3  10367  fzrevral2  10386  fzrevral3  10387  fzshftral  10388  fzoaddel2  10481  fzosubel  10485  fzosubel2  10486  fzocatel  10490  modqsubdir  10701  addmodlteq  10706  frecuzrdgsuc  10722  frecfzen2  10735  iseqovex  10766  seqvalcd  10769  seq3caopr3  10799  seqcaopr3g  10800  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seqf1oglem2  10828  seq3id3  10832  seqfeq3  10837  seq3distr  10840  ser3le  10845  mulexp  10886  mulexpzap  10887  expaddzap  10891  expubnd  10904  subsq  10954  binom2  10959  binom21  10960  binom2sub  10961  binom2sub1  10962  binom3  10965  sqoddm1div8  11001  mulsubdivbinom2ap  11019  nn0opthlem1d  11028  nn0opthd  11030  facp1  11038  facubnd  11053  bcval  11057  bcn1  11066  bcm1k  11068  bcp1n  11069  bcp1nk  11070  bcval5  11071  bcn2  11072  bcpasc  11074  hashun  11114  hashfz  11131  hashtpgim  11155  ccatlid  11232  ccatass  11234  ccat1st1st  11267  swrdval  11278  swrdspsleq  11297  ccatswrd  11300  pfxval  11304  addlenpfx  11321  ccatpfx  11331  ccatopth  11346  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccat  11365  swrdccat3blem  11369  swrdccatin2d  11374  pfxccatin12d  11375  cats1lend  11397  cats2catd  11399  s2eqd  11400  s3eqd  11401  s4eqd  11402  s5eqd  11403  s6eqd  11404  s7eqd  11405  s8eqd  11406  crre  11480  replim  11482  remullem  11494  remul2  11496  immul2  11503  cjcj  11506  cjadd  11507  ipcnval  11509  cjmulval  11511  cjneg  11513  imval2  11517  cjreim  11526  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrex  11649  sqabsadd  11678  sqabssub  11679  absreimsq  11690  recan  11732  amgm2  11741  maxabslemab  11829  maxabslemval  11831  max0addsup  11842  minabs  11859  bdtrilem  11862  bdtri  11863  xrmaxadd  11884  xrminadd  11898  xrbdtri  11899  subcn2  11934  reccn2ap  11936  climle  11957  climcvg1nlem  11972  serf0  11975  fsumadd  12030  fsumsplit  12031  sumpr  12037  sumtp  12038  isumadd  12055  sumsplitdc  12056  fsum2dlemstep  12058  fsumshftm  12069  fisumrev2  12070  fsumconst  12078  modfsummodlemstep  12081  telfsumo  12090  fsumparts  12094  binomlem  12107  binom  12108  binom1dif  12111  bcxmaslem1  12112  isumsplit  12115  isumnn0nn  12117  arisum  12122  arisum2  12123  trireciplem  12124  trirecip  12125  geosergap  12130  geo2sum  12138  geo2sum2  12139  cvgratnnlemsumlt  12152  mertenslemi1  12159  mertensabs  12161  fprodmul  12215  fprodsplitdc  12220  fprodabs  12240  fprod2dlemstep  12246  fproddivapf  12255  eftabs  12280  eftvalcn  12281  efcllemp  12282  ege2le3  12295  efcj  12297  efaddlem  12298  efsep  12315  ef4p  12318  efgt1p2  12319  efgt1p  12320  sinval  12326  cosval  12327  tanvalap  12332  tanval2ap  12337  tanval3ap  12338  efi4p  12341  sinneg  12350  cosneg  12351  tannegap  12352  efival  12356  efmival  12357  sinadd  12360  cosadd  12361  tanaddaplem  12362  tanaddap  12363  sinsub  12364  cossub  12365  addsin  12366  subsin  12367  sinmul  12368  cosmul  12369  addcos  12370  subcos  12371  sincossq  12372  cos2t  12374  sin01bnd  12381  cos01bnd  12382  efieq1re  12396  demoivreALT  12398  dvds2ln  12448  odd2np1lem  12496  bitsinv1lem  12585  gcdaddm  12618  bezoutlemnewy  12630  dfgcd3  12644  dvdsgcd  12646  mulgcd  12650  mulgcdr  12652  gcddiv  12653  sqgcd  12663  lcmgcdlem  12712  lcmgcd  12713  qredeu  12732  divgcdcoprm0  12736  cncongr1  12738  oddpwdclemdc  12808  sqrt2irraplemnn  12814  qnumdenbi  12827  zgcdsq  12836  hashdvds  12856  phiprmpw  12857  phimullem  12860  eulerthlema  12865  prmdiv  12870  modprm0  12890  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  pythagtriplem19  12918  pcval  12932  pcmul  12937  pcdiv  12938  pcqmul  12939  pcid  12960  pcaddlem  12975  pcmpt  12979  pcmpt2  12980  pcmptdvds  12981  pcbc  12987  4sqlem4  13028  mul4sqlem  13029  mul4sq  13030  4sqlem11  13037  4sqlem12  13038  4sqlem15  13041  4sqlem17  13043  ennnfonelemp1  13090  nninfdclemp1  13134  ressvalsets  13210  topnvalg  13397  topnpropgd  13399  prdsex  13415  prdsval  13419  pwsval  13437  qusval  13469  qusex  13471  qusaddvallemg  13479  xpsval  13498  gsumprval  13545  imasmnd2  13598  ismhm  13607  mhmf1o  13616  0mhm  13632  mhmco  13636  mhmeql  13638  gsumfzz  13641  isgrpid2  13686  grpnpcan  13738  imasgrp2  13760  mhmmnd  13766  mulgnndir  13801  mulgdir  13804  isnsg3  13857  isghm  13893  ghmnsgima  13918  ghmf1o  13925  conjghm  13926  qusghm  13932  ablsub4  13963  ghmcmn  13977  invghm  13979  gsumfzmptfidmadd  13989  gsumfzconst  13991  mgpvalg  14000  mgptopng  14006  mgpress  14008  rngdi  14017  rngdir  14018  rngpropd  14032  imasrng  14033  srglmhm  14070  srgrmhm  14071  ringo2times  14105  ringcom  14108  ringpropd  14115  ring1  14136  ringlghm  14138  ringrghm  14139  imasring  14141  opprvalg  14146  opprrng  14154  opprring  14156  invrfvald  14200  dvrvald  14212  dvrdir  14221  rdivmuldivd  14222  islmod  14370  lmodlema  14371  islmodd  14372  lmodcom  14412  lmodnegadd  14415  lmodprop2d  14427  rmodislmod  14430  lsssn0  14449  sraval  14516  qusrhm  14607  gsumfzfsumlemm  14666  expghmap  14686  mulgghm2  14687  mulgrhm  14688  zlmval  14706  znval  14715  psrval  14745  mplvalcoe  14774  cnfval  14988  cnpfval  14989  ispsmet  15117  psmet0  15121  psmettri2  15122  psmetres2  15127  ismet  15138  isxmet  15139  xmettri2  15155  xmetres2  15173  xblss2  15199  xmstri2  15264  mstri2  15265  xmstri  15266  mstri  15267  xmstri3  15268  mstri3  15269  msrtri  15270  comet  15293  bdxmet  15295  txmetcnp  15312  metcnpd  15314  cnmet  15324  ioo2bl  15345  mpomulcn  15360  fsumcncntop  15361  elcncf  15367  mulc1cncf  15383  cncfco  15385  cncfcncntop  15387  cncfmptc  15390  cncfmptid  15391  addccncf  15394  cdivcncfap  15398  negcncf  15399  mulcncflem  15401  limccnp2cntop  15471  reldvg  15473  dvfvalap  15475  eldvap  15476  dvconst  15488  dvconstre  15490  dvconstss  15492  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvexp  15505  dvrecap  15507  dvmptid  15510  dvmptc  15511  dveflem  15520  dvef  15521  elplyd  15535  ply1termlem  15536  plyaddlem1  15541  plymullem1  15542  plyadd  15545  plymul  15546  plycoeid3  15551  plycolemc  15552  plyco  15553  plycjlemc  15554  plycj  15555  plyrecj  15557  dvply1  15559  dvply2g  15560  sinperlem  15602  sinmpi  15609  cosmpi  15610  sinppi  15611  cosppi  15612  efimpi  15613  sinhalfpip  15614  sinhalfpim  15615  coshalfpip  15616  coshalfpim  15617  ptolemy  15618  tangtx  15632  logdivlti  15675  rpcxpadd  15699  rpmulcxp  15703  rplogbchbase  15744  rprelogbmul  15749  binom4  15773  pellexlem2  15775  pellexlem3  15776  wilthlem1  15777  1sgmprm  15791  1sgm2ppw  15792  sgmmul  15793  mersenne  15794  perfect1  15795  perfectlem2  15797  perfect  15798  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsval4a  15824  lgsneg  15826  lgsdilem  15829  lgsdirprm  15836  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  gausslemma2dlem4  15866  gausslemma2dlem6  15869  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  lgsquad2lem2  15884  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2sqlem2  15917  2sqlem3  15919  2sqlem4  15920  2sqlem8  15925  vtxdgfval  16212  vtxdgfifival  16215  vtxdgop  16216  vtxdgfi0e  16219  vtxdeqd  16220  vtxdfifiun  16221  vtxduspgrfvedgfi  16225  1loopgrvd2fi  16229  repiecele0  16741  repiecege0  16742  repiecef  16743  cvgcmp2nlemabs  16747  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trilpo  16758  redcwlpo  16771  nconstwlpolemgt0  16780  nconstwlpo  16782  neapmkv  16784  gsumgfsum  16796  gfsump1  16798