Theorem oveq12d 5943

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5925

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveq123d  5946  ovmpodxf  6052  ovmpodf  6058  caovdig  6102  caovdir2d  6104  caovdirg  6105  caovdilemd  6119  caovlem2d  6120  offval  6147  ofvalg  6149  offval2  6155  ofco  6158  caofinvl  6165  offres  6201  nnmsucr  6555  nndir  6557  ecovdi  6714  ecovidi  6715  dfplpq2  7438  dfmpq2  7439  addcmpblnq  7451  mulpipqqs  7457  addassnqg  7466  distrnqg  7471  ltaddnq  7491  halfnqq  7494  enq0tr  7518  addcmpblnq0  7527  addnq0mo  7531  addnnnq0  7533  nqnq0a  7538  distrnq0  7543  addassnq0  7546  distnq0r  7547  nq02m  7549  ltexpri  7697  cauappcvgprlemm  7729  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemmu  7779  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem2  7794  mulcmpblnrlemg  7824  mulsrmo  7828  mulsrpr  7830  mulcomsrg  7841  distrsrg  7843  recexgt0sr  7857  mulgt0sr  7862  mulextsr1lem  7864  caucvgsrlemgt1  7879  caucvgsr  7886  addcnsr  7918  mulcnsr  7919  recidpirqlemcalc  7941  axaddcl  7948  axmulcl  7950  axmulcom  7955  axmulass  7957  axdistr  7958  axcaucvglemcau  7982  axcaucvglemres  7983  adddir  8034  muladd11  8176  1p1times  8177  muladd11r  8199  pnpcan2  8283  muladd  8427  subdir  8429  mulsub  8444  mulreim  8648  apadd1  8652  mulext1  8656  recextlem1  8695  muleqadd  8712  divdirap  8741  divadddivap  8771  conjmulap  8773  divcanap5rd  8862  subrecap  8883  xp1d2m1eqxm1d2  9261  div4p1lem1div2  9262  cnref1o  9742  xnegid  9951  xposdif  9974  xleaddadd  9979  icoshftf1o  10083  lincmb01cmp  10095  iccf1o  10096  fz01en  10145  fzrev3  10179  fzrevral2  10198  fzrevral3  10199  fzshftral  10200  fzoaddel2  10286  fzosubel  10287  fzosubel2  10288  fzocatel  10292  modqsubdir  10502  addmodlteq  10507  frecuzrdgsuc  10523  frecfzen2  10536  iseqovex  10567  seqvalcd  10570  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seqf1oglem2  10629  seq3id3  10633  seqfeq3  10638  seq3distr  10641  ser3le  10646  mulexp  10687  mulexpzap  10688  expaddzap  10692  expubnd  10705  subsq  10755  binom2  10760  binom21  10761  binom2sub  10762  binom2sub1  10763  binom3  10766  sqoddm1div8  10802  mulsubdivbinom2ap  10820  nn0opthlem1d  10829  nn0opthd  10831  facp1  10839  facubnd  10854  bcval  10858  bcn1  10867  bcm1k  10869  bcp1n  10870  bcp1nk  10871  bcval5  10872  bcn2  10873  bcpasc  10875  hashun  10914  hashfz  10930  crre  11039  replim  11041  remullem  11053  remul2  11055  immul2  11062  cjcj  11065  cjadd  11066  ipcnval  11068  cjmulval  11070  cjneg  11072  imval2  11076  cjreim  11085  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemp1rp  11188  resqrexlemfp1  11191  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrex  11208  sqabsadd  11237  sqabssub  11238  absreimsq  11249  recan  11291  amgm2  11300  maxabslemab  11388  maxabslemval  11390  max0addsup  11401  minabs  11418  bdtrilem  11421  bdtri  11422  xrmaxadd  11443  xrminadd  11457  xrbdtri  11458  subcn2  11493  reccn2ap  11495  climle  11516  climcvg1nlem  11531  serf0  11534  fsumadd  11588  fsumsplit  11589  sumpr  11595  sumtp  11596  isumadd  11613  sumsplitdc  11614  fsum2dlemstep  11616  fsumshftm  11627  fisumrev2  11628  fsumconst  11636  modfsummodlemstep  11639  telfsumo  11648  fsumparts  11652  binomlem  11665  binom  11666  binom1dif  11669  bcxmaslem1  11670  isumsplit  11673  isumnn0nn  11675  arisum  11680  arisum2  11681  trireciplem  11682  trirecip  11683  geosergap  11688  geo2sum  11696  geo2sum2  11697  cvgratnnlemsumlt  11710  mertenslemi1  11717  mertensabs  11719  fprodmul  11773  fprodsplitdc  11778  fprodabs  11798  fprod2dlemstep  11804  fproddivapf  11813  eftabs  11838  eftvalcn  11839  efcllemp  11840  ege2le3  11853  efcj  11855  efaddlem  11856  efsep  11873  ef4p  11876  efgt1p2  11877  efgt1p  11878  sinval  11884  cosval  11885  tanvalap  11890  tanval2ap  11895  tanval3ap  11896  efi4p  11899  sinneg  11908  cosneg  11909  tannegap  11910  efival  11914  efmival  11915  sinadd  11918  cosadd  11919  tanaddaplem  11920  tanaddap  11921  sinsub  11922  cossub  11923  addsin  11924  subsin  11925  sinmul  11926  cosmul  11927  addcos  11928  subcos  11929  sincossq  11930  cos2t  11932  sin01bnd  11939  cos01bnd  11940  efieq1re  11954  demoivreALT  11956  dvds2ln  12006  odd2np1lem  12054  bitsinv1lem  12143  gcdaddm  12176  bezoutlemnewy  12188  dfgcd3  12202  dvdsgcd  12204  mulgcd  12208  mulgcdr  12210  gcddiv  12211  sqgcd  12221  lcmgcdlem  12270  lcmgcd  12271  qredeu  12290  divgcdcoprm0  12294  cncongr1  12296  oddpwdclemdc  12366  sqrt2irraplemnn  12372  qnumdenbi  12385  zgcdsq  12394  hashdvds  12414  phiprmpw  12415  phimullem  12418  eulerthlema  12423  prmdiv  12428  modprm0  12448  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  pythagtriplem19  12476  pcval  12490  pcmul  12495  pcdiv  12496  pcqmul  12497  pcid  12518  pcaddlem  12533  pcmpt  12537  pcmpt2  12538  pcmptdvds  12539  pcbc  12545  4sqlem4  12586  mul4sqlem  12587  mul4sq  12588  4sqlem11  12595  4sqlem12  12596  4sqlem15  12599  4sqlem17  12601  ennnfonelemp1  12648  nninfdclemp1  12692  ressvalsets  12767  topnvalg  12953  topnpropgd  12955  prdsex  12971  prdsval  12975  pwsval  12993  qusval  13025  qusex  13027  qusaddvallemg  13035  xpsval  13054  gsumprval  13101  imasmnd2  13154  ismhm  13163  mhmf1o  13172  0mhm  13188  mhmco  13192  mhmeql  13194  gsumfzz  13197  isgrpid2  13242  grpnpcan  13294  imasgrp2  13316  mhmmnd  13322  mulgnndir  13357  mulgdir  13360  isnsg3  13413  isghm  13449  ghmnsgima  13474  ghmf1o  13481  conjghm  13482  qusghm  13488  ablsub4  13519  ghmcmn  13533  invghm  13535  gsumfzmptfidmadd  13545  gsumfzconst  13547  mgpvalg  13555  mgptopng  13561  mgpress  13563  rngdi  13572  rngdir  13573  rngpropd  13587  imasrng  13588  srglmhm  13625  srgrmhm  13626  ringo2times  13660  ringcom  13663  ringpropd  13670  ring1  13691  ringlghm  13693  ringrghm  13694  imasring  13696  opprvalg  13701  opprrng  13709  opprring  13711  invrfvald  13754  dvrvald  13766  dvrdir  13775  rdivmuldivd  13776  islmod  13923  lmodlema  13924  islmodd  13925  lmodcom  13965  lmodnegadd  13968  lmodprop2d  13980  rmodislmod  13983  lsssn0  14002  sraval  14069  qusrhm  14160  gsumfzfsumlemm  14219  expghmap  14239  mulgghm2  14240  mulgrhm  14241  zlmval  14259  znval  14268  psrval  14296  cnfval  14514  cnpfval  14515  ispsmet  14643  psmet0  14647  psmettri2  14648  psmetres2  14653  ismet  14664  isxmet  14665  xmettri2  14681  xmetres2  14699  xblss2  14725  xmstri2  14790  mstri2  14791  xmstri  14792  mstri  14793  xmstri3  14794  mstri3  14795  msrtri  14796  comet  14819  bdxmet  14821  txmetcnp  14838  metcnpd  14840  cnmet  14850  ioo2bl  14871  mpomulcn  14886  fsumcncntop  14887  elcncf  14893  mulc1cncf  14909  cncfco  14911  cncfcncntop  14913  cncfmptc  14916  cncfmptid  14917  addccncf  14920  cdivcncfap  14924  negcncf  14925  mulcncflem  14927  limccnp2cntop  14997  reldvg  14999  dvfvalap  15001  eldvap  15002  dvconst  15014  dvconstre  15016  dvconstss  15018  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvexp  15031  dvrecap  15033  dvmptid  15036  dvmptc  15037  dveflem  15046  dvef  15047  elplyd  15061  ply1termlem  15062  plyaddlem1  15067  plymullem1  15068  plyadd  15071  plymul  15072  plycoeid3  15077  plycolemc  15078  plyco  15079  plycjlemc  15080  plycj  15081  plyrecj  15083  dvply1  15085  dvply2g  15086  sinperlem  15128  sinmpi  15135  cosmpi  15136  sinppi  15137  cosppi  15138  efimpi  15139  sinhalfpip  15140  sinhalfpim  15141  coshalfpip  15142  coshalfpim  15143  ptolemy  15144  tangtx  15158  logdivlti  15201  rpcxpadd  15225  rpmulcxp  15229  rplogbchbase  15270  rprelogbmul  15275  binom4  15299  wilthlem1  15300  1sgmprm  15314  1sgm2ppw  15315  sgmmul  15316  mersenne  15317  perfect1  15318  perfectlem2  15320  perfect  15321  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsval4a  15347  lgsneg  15349  lgsdilem  15352  lgsdirprm  15359  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  gausslemma2dlem4  15389  gausslemma2dlem6  15392  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  lgsquad2lem2  15407  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2sqlem2  15440  2sqlem3  15442  2sqlem4  15443  2sqlem8  15448  cvgcmp2nlemabs  15763  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trilpo  15774  redcwlpo  15786  nconstwlpolemgt0  15795  nconstwlpo  15797  neapmkv  15799