Theorem oveq12d 5961

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

Syntax hints:   → wi 4   = wceq 1372  (class class class)co 5943

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  oveq123d  5964  ovmpodxf  6070  ovmpodf  6076  caovdig  6120  caovdir2d  6122  caovdirg  6123  caovdilemd  6137  caovlem2d  6138  offval  6165  ofvalg  6167  offval2  6173  ofco  6176  caofinvl  6183  offres  6219  nnmsucr  6573  nndir  6575  ecovdi  6732  ecovidi  6733  dfplpq2  7466  dfmpq2  7467  addcmpblnq  7479  mulpipqqs  7485  addassnqg  7494  distrnqg  7499  ltaddnq  7519  halfnqq  7522  enq0tr  7546  addcmpblnq0  7555  addnq0mo  7559  addnnnq0  7561  nqnq0a  7566  distrnq0  7571  addassnq0  7574  distnq0r  7575  nq02m  7577  ltexpri  7725  cauappcvgprlemm  7757  cauappcvgprlemloc  7764  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  cauappcvgprlemlim  7773  cauappcvgpr  7774  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemloc  7787  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem2  7792  caucvgpr  7794  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemmu  7807  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem2  7822  mulcmpblnrlemg  7852  mulsrmo  7856  mulsrpr  7858  mulcomsrg  7869  distrsrg  7871  recexgt0sr  7885  mulgt0sr  7890  mulextsr1lem  7892  caucvgsrlemgt1  7907  caucvgsr  7914  addcnsr  7946  mulcnsr  7947  recidpirqlemcalc  7969  axaddcl  7976  axmulcl  7978  axmulcom  7983  axmulass  7985  axdistr  7986  axcaucvglemcau  8010  axcaucvglemres  8011  adddir  8062  muladd11  8204  1p1times  8205  muladd11r  8227  pnpcan2  8311  muladd  8455  subdir  8457  mulsub  8472  mulreim  8676  apadd1  8680  mulext1  8684  recextlem1  8723  muleqadd  8740  divdirap  8769  divadddivap  8799  conjmulap  8801  divcanap5rd  8890  subrecap  8911  xp1d2m1eqxm1d2  9289  div4p1lem1div2  9290  cnref1o  9771  xnegid  9980  xposdif  10003  xleaddadd  10008  icoshftf1o  10112  lincmb01cmp  10124  iccf1o  10125  fz01en  10174  fzrev3  10208  fzrevral2  10227  fzrevral3  10228  fzshftral  10229  fzoaddel2  10317  fzosubel  10321  fzosubel2  10322  fzocatel  10326  modqsubdir  10536  addmodlteq  10541  frecuzrdgsuc  10557  frecfzen2  10570  iseqovex  10601  seqvalcd  10604  seq3caopr3  10634  seqcaopr3g  10635  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seqf1oglem2  10663  seq3id3  10667  seqfeq3  10672  seq3distr  10675  ser3le  10680  mulexp  10721  mulexpzap  10722  expaddzap  10726  expubnd  10739  subsq  10789  binom2  10794  binom21  10795  binom2sub  10796  binom2sub1  10797  binom3  10800  sqoddm1div8  10836  mulsubdivbinom2ap  10854  nn0opthlem1d  10863  nn0opthd  10865  facp1  10873  facubnd  10888  bcval  10892  bcn1  10901  bcm1k  10903  bcp1n  10904  bcp1nk  10905  bcval5  10906  bcn2  10907  bcpasc  10909  hashun  10948  hashfz  10964  ccatlid  11060  ccatass  11062  ccat1st1st  11091  crre  11139  replim  11141  remullem  11153  remul2  11155  immul2  11162  cjcj  11165  cjadd  11166  ipcnval  11168  cjmulval  11170  cjneg  11172  imval2  11176  cjreim  11185  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemp1rp  11288  resqrexlemfp1  11291  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrex  11308  sqabsadd  11337  sqabssub  11338  absreimsq  11349  recan  11391  amgm2  11400  maxabslemab  11488  maxabslemval  11490  max0addsup  11501  minabs  11518  bdtrilem  11521  bdtri  11522  xrmaxadd  11543  xrminadd  11557  xrbdtri  11558  subcn2  11593  reccn2ap  11595  climle  11616  climcvg1nlem  11631  serf0  11634  fsumadd  11688  fsumsplit  11689  sumpr  11695  sumtp  11696  isumadd  11713  sumsplitdc  11714  fsum2dlemstep  11716  fsumshftm  11727  fisumrev2  11728  fsumconst  11736  modfsummodlemstep  11739  telfsumo  11748  fsumparts  11752  binomlem  11765  binom  11766  binom1dif  11769  bcxmaslem1  11770  isumsplit  11773  isumnn0nn  11775  arisum  11780  arisum2  11781  trireciplem  11782  trirecip  11783  geosergap  11788  geo2sum  11796  geo2sum2  11797  cvgratnnlemsumlt  11810  mertenslemi1  11817  mertensabs  11819  fprodmul  11873  fprodsplitdc  11878  fprodabs  11898  fprod2dlemstep  11904  fproddivapf  11913  eftabs  11938  eftvalcn  11939  efcllemp  11940  ege2le3  11953  efcj  11955  efaddlem  11956  efsep  11973  ef4p  11976  efgt1p2  11977  efgt1p  11978  sinval  11984  cosval  11985  tanvalap  11990  tanval2ap  11995  tanval3ap  11996  efi4p  11999  sinneg  12008  cosneg  12009  tannegap  12010  efival  12014  efmival  12015  sinadd  12018  cosadd  12019  tanaddaplem  12020  tanaddap  12021  sinsub  12022  cossub  12023  addsin  12024  subsin  12025  sinmul  12026  cosmul  12027  addcos  12028  subcos  12029  sincossq  12030  cos2t  12032  sin01bnd  12039  cos01bnd  12040  efieq1re  12054  demoivreALT  12056  dvds2ln  12106  odd2np1lem  12154  bitsinv1lem  12243  gcdaddm  12276  bezoutlemnewy  12288  dfgcd3  12302  dvdsgcd  12304  mulgcd  12308  mulgcdr  12310  gcddiv  12311  sqgcd  12321  lcmgcdlem  12370  lcmgcd  12371  qredeu  12390  divgcdcoprm0  12394  cncongr1  12396  oddpwdclemdc  12466  sqrt2irraplemnn  12472  qnumdenbi  12485  zgcdsq  12494  hashdvds  12514  phiprmpw  12515  phimullem  12518  eulerthlema  12523  prmdiv  12528  modprm0  12548  coprimeprodsq  12551  pythagtriplem1  12559  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem15  12572  pythagtriplem16  12573  pythagtriplem17  12574  pythagtriplem19  12576  pcval  12590  pcmul  12595  pcdiv  12596  pcqmul  12597  pcid  12618  pcaddlem  12633  pcmpt  12637  pcmpt2  12638  pcmptdvds  12639  pcbc  12645  4sqlem4  12686  mul4sqlem  12687  mul4sq  12688  4sqlem11  12695  4sqlem12  12696  4sqlem15  12699  4sqlem17  12701  ennnfonelemp1  12748  nninfdclemp1  12792  ressvalsets  12867  topnvalg  13054  topnpropgd  13056  prdsex  13072  prdsval  13076  pwsval  13094  qusval  13126  qusex  13128  qusaddvallemg  13136  xpsval  13155  gsumprval  13202  imasmnd2  13255  ismhm  13264  mhmf1o  13273  0mhm  13289  mhmco  13293  mhmeql  13295  gsumfzz  13298  isgrpid2  13343  grpnpcan  13395  imasgrp2  13417  mhmmnd  13423  mulgnndir  13458  mulgdir  13461  isnsg3  13514  isghm  13550  ghmnsgima  13575  ghmf1o  13582  conjghm  13583  qusghm  13589  ablsub4  13620  ghmcmn  13634  invghm  13636  gsumfzmptfidmadd  13646  gsumfzconst  13648  mgpvalg  13656  mgptopng  13662  mgpress  13664  rngdi  13673  rngdir  13674  rngpropd  13688  imasrng  13689  srglmhm  13726  srgrmhm  13727  ringo2times  13761  ringcom  13764  ringpropd  13771  ring1  13792  ringlghm  13794  ringrghm  13795  imasring  13797  opprvalg  13802  opprrng  13810  opprring  13812  invrfvald  13855  dvrvald  13867  dvrdir  13876  rdivmuldivd  13877  islmod  14024  lmodlema  14025  islmodd  14026  lmodcom  14066  lmodnegadd  14069  lmodprop2d  14081  rmodislmod  14084  lsssn0  14103  sraval  14170  qusrhm  14261  gsumfzfsumlemm  14320  expghmap  14340  mulgghm2  14341  mulgrhm  14342  zlmval  14360  znval  14369  psrval  14399  mplvalcoe  14423  cnfval  14637  cnpfval  14638  ispsmet  14766  psmet0  14770  psmettri2  14771  psmetres2  14776  ismet  14787  isxmet  14788  xmettri2  14804  xmetres2  14822  xblss2  14848  xmstri2  14913  mstri2  14914  xmstri  14915  mstri  14916  xmstri3  14917  mstri3  14918  msrtri  14919  comet  14942  bdxmet  14944  txmetcnp  14961  metcnpd  14963  cnmet  14973  ioo2bl  14994  mpomulcn  15009  fsumcncntop  15010  elcncf  15016  mulc1cncf  15032  cncfco  15034  cncfcncntop  15036  cncfmptc  15039  cncfmptid  15040  addccncf  15043  cdivcncfap  15047  negcncf  15048  mulcncflem  15050  limccnp2cntop  15120  reldvg  15122  dvfvalap  15124  eldvap  15125  dvconst  15137  dvconstre  15139  dvconstss  15141  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvexp  15154  dvrecap  15156  dvmptid  15159  dvmptc  15160  dveflem  15169  dvef  15170  elplyd  15184  ply1termlem  15185  plyaddlem1  15190  plymullem1  15191  plyadd  15194  plymul  15195  plycoeid3  15200  plycolemc  15201  plyco  15202  plycjlemc  15203  plycj  15204  plyrecj  15206  dvply1  15208  dvply2g  15209  sinperlem  15251  sinmpi  15258  cosmpi  15259  sinppi  15260  cosppi  15261  efimpi  15262  sinhalfpip  15263  sinhalfpim  15264  coshalfpip  15265  coshalfpim  15266  ptolemy  15267  tangtx  15281  logdivlti  15324  rpcxpadd  15348  rpmulcxp  15352  rplogbchbase  15393  rprelogbmul  15398  binom4  15422  wilthlem1  15423  1sgmprm  15437  1sgm2ppw  15438  sgmmul  15439  mersenne  15440  perfect1  15441  perfectlem2  15443  perfect  15444  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsval4a  15470  lgsneg  15472  lgsdilem  15475  lgsdirprm  15482  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  gausslemma2dlem4  15512  gausslemma2dlem6  15515  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  lgsquad2lem2  15530  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2sqlem2  15563  2sqlem3  15565  2sqlem4  15566  2sqlem8  15571  cvgcmp2nlemabs  15933  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trilpo  15944  redcwlpo  15956  nconstwlpolemgt0  15965  nconstwlpo  15967  neapmkv  15969