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  crre  11110  replim  11112  remullem  11124  remul2  11126  immul2  11133  cjcj  11136  cjadd  11137  ipcnval  11139  cjmulval  11141  cjneg  11143  imval2  11147  cjreim  11156  cvg1nlemcau  11237  cvg1nlemres  11238  resqrexlemp1rp  11259  resqrexlemfp1  11262  resqrexlemcalc1  11267  resqrexlemcalc2  11268  resqrex  11279  sqabsadd  11308  sqabssub  11309  absreimsq  11320  recan  11362  amgm2  11371  maxabslemab  11459  maxabslemval  11461  max0addsup  11472  minabs  11489  bdtrilem  11492  bdtri  11493  xrmaxadd  11514  xrminadd  11528  xrbdtri  11529  subcn2  11564  reccn2ap  11566  climle  11587  climcvg1nlem  11602  serf0  11605  fsumadd  11659  fsumsplit  11660  sumpr  11666  sumtp  11667  isumadd  11684  sumsplitdc  11685  fsum2dlemstep  11687  fsumshftm  11698  fisumrev2  11699  fsumconst  11707  modfsummodlemstep  11710  telfsumo  11719  fsumparts  11723  binomlem  11736  binom  11737  binom1dif  11740  bcxmaslem1  11741  isumsplit  11744  isumnn0nn  11746  arisum  11751  arisum2  11752  trireciplem  11753  trirecip  11754  geosergap  11759  geo2sum  11767  geo2sum2  11768  cvgratnnlemsumlt  11781  mertenslemi1  11788  mertensabs  11790  fprodmul  11844  fprodsplitdc  11849  fprodabs  11869  fprod2dlemstep  11875  fproddivapf  11884  eftabs  11909  eftvalcn  11910  efcllemp  11911  ege2le3  11924  efcj  11926  efaddlem  11927  efsep  11944  ef4p  11947  efgt1p2  11948  efgt1p  11949  sinval  11955  cosval  11956  tanvalap  11961  tanval2ap  11966  tanval3ap  11967  efi4p  11970  sinneg  11979  cosneg  11980  tannegap  11981  efival  11985  efmival  11986  sinadd  11989  cosadd  11990  tanaddaplem  11991  tanaddap  11992  sinsub  11993  cossub  11994  addsin  11995  subsin  11996  sinmul  11997  cosmul  11998  addcos  11999  subcos  12000  sincossq  12001  cos2t  12003  sin01bnd  12010  cos01bnd  12011  efieq1re  12025  demoivreALT  12027  dvds2ln  12077  odd2np1lem  12125  bitsinv1lem  12214  gcdaddm  12247  bezoutlemnewy  12259  dfgcd3  12273  dvdsgcd  12275  mulgcd  12279  mulgcdr  12281  gcddiv  12282  sqgcd  12292  lcmgcdlem  12341  lcmgcd  12342  qredeu  12361  divgcdcoprm0  12365  cncongr1  12367  oddpwdclemdc  12437  sqrt2irraplemnn  12443  qnumdenbi  12456  zgcdsq  12465  hashdvds  12485  phiprmpw  12486  phimullem  12489  eulerthlema  12494  prmdiv  12499  modprm0  12519  coprimeprodsq  12522  pythagtriplem1  12530  pythagtriplem12  12540  pythagtriplem14  12542  pythagtriplem15  12543  pythagtriplem16  12544  pythagtriplem17  12545  pythagtriplem19  12547  pcval  12561  pcmul  12566  pcdiv  12567  pcqmul  12568  pcid  12589  pcaddlem  12604  pcmpt  12608  pcmpt2  12609  pcmptdvds  12610  pcbc  12616  4sqlem4  12657  mul4sqlem  12658  mul4sq  12659  4sqlem11  12666  4sqlem12  12667  4sqlem15  12670  4sqlem17  12672  ennnfonelemp1  12719  nninfdclemp1  12763  ressvalsets  12838  topnvalg  13025  topnpropgd  13027  prdsex  13043  prdsval  13047  pwsval  13065  qusval  13097  qusex  13099  qusaddvallemg  13107  xpsval  13126  gsumprval  13173  imasmnd2  13226  ismhm  13235  mhmf1o  13244  0mhm  13260  mhmco  13264  mhmeql  13266  gsumfzz  13269  isgrpid2  13314  grpnpcan  13366  imasgrp2  13388  mhmmnd  13394  mulgnndir  13429  mulgdir  13432  isnsg3  13485  isghm  13521  ghmnsgima  13546  ghmf1o  13553  conjghm  13554  qusghm  13560  ablsub4  13591  ghmcmn  13605  invghm  13607  gsumfzmptfidmadd  13617  gsumfzconst  13619  mgpvalg  13627  mgptopng  13633  mgpress  13635  rngdi  13644  rngdir  13645  rngpropd  13659  imasrng  13660  srglmhm  13697  srgrmhm  13698  ringo2times  13732  ringcom  13735  ringpropd  13742  ring1  13763  ringlghm  13765  ringrghm  13766  imasring  13768  opprvalg  13773  opprrng  13781  opprring  13783  invrfvald  13826  dvrvald  13838  dvrdir  13847  rdivmuldivd  13848  islmod  13995  lmodlema  13996  islmodd  13997  lmodcom  14037  lmodnegadd  14040  lmodprop2d  14052  rmodislmod  14055  lsssn0  14074  sraval  14141  qusrhm  14232  gsumfzfsumlemm  14291  expghmap  14311  mulgghm2  14312  mulgrhm  14313  zlmval  14331  znval  14340  psrval  14370  mplvalcoe  14394  cnfval  14608  cnpfval  14609  ispsmet  14737  psmet0  14741  psmettri2  14742  psmetres2  14747  ismet  14758  isxmet  14759  xmettri2  14775  xmetres2  14793  xblss2  14819  xmstri2  14884  mstri2  14885  xmstri  14886  mstri  14887  xmstri3  14888  mstri3  14889  msrtri  14890  comet  14913  bdxmet  14915  txmetcnp  14932  metcnpd  14934  cnmet  14944  ioo2bl  14965  mpomulcn  14980  fsumcncntop  14981  elcncf  14987  mulc1cncf  15003  cncfco  15005  cncfcncntop  15007  cncfmptc  15010  cncfmptid  15011  addccncf  15014  cdivcncfap  15018  negcncf  15019  mulcncflem  15021  limccnp2cntop  15091  reldvg  15093  dvfvalap  15095  eldvap  15096  dvconst  15108  dvconstre  15110  dvconstss  15112  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvcjbr  15122  dvexp  15125  dvrecap  15127  dvmptid  15130  dvmptc  15131  dveflem  15140  dvef  15141  elplyd  15155  ply1termlem  15156  plyaddlem1  15161  plymullem1  15162  plyadd  15165  plymul  15166  plycoeid3  15171  plycolemc  15172  plyco  15173  plycjlemc  15174  plycj  15175  plyrecj  15177  dvply1  15179  dvply2g  15180  sinperlem  15222  sinmpi  15229  cosmpi  15230  sinppi  15231  cosppi  15232  efimpi  15233  sinhalfpip  15234  sinhalfpim  15235  coshalfpip  15236  coshalfpim  15237  ptolemy  15238  tangtx  15252  logdivlti  15295  rpcxpadd  15319  rpmulcxp  15323  rplogbchbase  15364  rprelogbmul  15369  binom4  15393  wilthlem1  15394  1sgmprm  15408  1sgm2ppw  15409  sgmmul  15410  mersenne  15411  perfect1  15412  perfectlem2  15414  perfect  15415  lgsval  15423  lgsfvalg  15424  lgsval2lem  15429  lgsval4a  15441  lgsneg  15443  lgsdilem  15446  lgsdirprm  15453  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  gausslemma2dlem4  15483  gausslemma2dlem6  15486  lgseisenlem2  15490  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  lgsquad2lem1  15500  lgsquad2lem2  15501  2lgslem3a  15512  2lgslem3b  15513  2lgslem3c  15514  2lgslem3d  15515  2sqlem2  15534  2sqlem3  15536  2sqlem4  15537  2sqlem8  15542  cvgcmp2nlemabs  15904  trilpolemclim  15908  trilpolemcl  15909  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  trilpo  15915  redcwlpo  15927  nconstwlpolemgt0  15936  nconstwlpo  15938  neapmkv  15940