Theorem oveq12d 6076

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6058

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  oveq123d  6079  ovmpodxf  6187  ovmpodf  6193  caovdig  6237  caovdir2d  6239  caovdirg  6240  caovdilemd  6254  caovlem2d  6255  offval  6283  ofvalg  6285  offval2  6291  ofco  6294  caofinvl  6301  offres  6341  nnmsucr  6734  nndir  6736  ecovdi  6893  ecovidi  6894  dfplpq2  7685  dfmpq2  7686  addcmpblnq  7698  mulpipqqs  7704  addassnqg  7713  distrnqg  7718  ltaddnq  7738  halfnqq  7741  enq0tr  7765  addcmpblnq0  7774  addnq0mo  7778  addnnnq0  7780  nqnq0a  7785  distrnq0  7790  addassnq0  7793  distnq0r  7794  nq02m  7796  ltexpri  7944  cauappcvgprlemm  7976  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemmu  8026  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem2  8041  mulcmpblnrlemg  8071  mulsrmo  8075  mulsrpr  8077  mulcomsrg  8088  distrsrg  8090  recexgt0sr  8104  mulgt0sr  8109  mulextsr1lem  8111  caucvgsrlemgt1  8126  caucvgsr  8133  addcnsr  8165  mulcnsr  8166  recidpirqlemcalc  8188  axaddcl  8195  axmulcl  8197  axmulcom  8202  axmulass  8204  axdistr  8205  axcaucvglemcau  8229  axcaucvglemres  8230  adddir  8281  muladd11  8422  1p1times  8423  muladd11r  8445  pnpcan2  8529  muladd  8674  subdir  8676  mulsub  8691  mulreim  8895  apadd1  8899  mulext1  8903  recextlem1  8942  muleqadd  8959  divdirap  8988  divadddivap  9018  conjmulap  9020  divcanap5rd  9109  subrecap  9130  xp1d2m1eqxm1d2  9508  div4p1lem1div2  9509  cnref1o  10001  xnegid  10211  xposdif  10234  xleaddadd  10239  icoshftf1o  10343  lincmb01cmp  10355  iccf1o  10357  fz01en  10408  fzrev3  10443  fzrevral2  10462  fzrevral3  10463  fzshftral  10464  fzoaddel2  10557  fzosubel  10561  fzosubel2  10562  fzocatel  10566  modqsubdir  10779  addmodlteq  10784  frecuzrdgsuc  10800  frecfzen2  10813  iseqovex  10844  seqvalcd  10847  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seqf1oglem2  10906  seq3id3  10910  seqfeq3  10915  seq3distr  10918  ser3le  10923  mulexp  10964  mulexpzap  10965  expaddzap  10969  expubnd  10982  subsq  11032  binom2  11037  binom21  11038  binom2sub  11039  binom2sub1  11040  binom3  11043  sqoddm1div8  11080  mulsubdivbinom2ap  11098  nn0opthlem1d  11107  nn0opthd  11109  facp1  11117  facubnd  11132  bcval  11136  bcn1  11145  bcm1k  11147  bcp1n  11148  bcp1nk  11149  bcval5  11150  bcn2  11151  bcpasc  11153  bcm1n  11156  hashun  11194  hashfz  11211  hashfibclem  11231  hashfibc  11232  hashtpgim  11242  ccatlid  11319  ccatass  11321  ccat1st1st  11354  swrdval  11365  swrdspsleq  11384  ccatswrd  11387  pfxval  11391  addlenpfx  11408  ccatpfx  11418  ccatopth  11433  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat  11452  swrdccat3blem  11456  swrdccatin2d  11461  pfxccatin12d  11462  cats1lend  11484  cats2catd  11486  s2eqd  11487  s3eqd  11488  s4eqd  11489  s5eqd  11490  s6eqd  11491  s7eqd  11492  s8eqd  11493  crre  11567  replim  11569  remullem  11581  remul2  11583  immul2  11590  cjcj  11593  cjadd  11594  ipcnval  11596  cjmulval  11598  cjneg  11600  imval2  11604  cjreim  11613  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrex  11736  sqabsadd  11765  sqabssub  11766  absreimsq  11777  recan  11819  amgm2  11828  maxabslemab  11916  maxabslemval  11918  max0addsup  11929  minabs  11946  bdtrilem  11949  bdtri  11950  xrmaxadd  11971  xrminadd  11985  xrbdtri  11986  subcn2  12021  reccn2ap  12023  climle  12044  climcvg1nlem  12059  serf0  12062  fsumadd  12117  fsumsplit  12118  sumpr  12124  sumtp  12125  isumadd  12142  sumsplitdc  12143  fsum2dlemstep  12145  fsumshftm  12156  fisumrev2  12157  fsumconst  12165  modfsummodlemstep  12168  telfsumo  12177  fsumparts  12181  binomlem  12194  binom  12195  binom1dif  12198  bcxmaslem1  12199  isumsplit  12202  isumnn0nn  12204  arisum  12209  arisum2  12210  trireciplem  12211  trirecip  12212  geosergap  12217  geo2sum  12225  geo2sum2  12226  cvgratnnlemsumlt  12239  mertenslemi1  12246  mertensabs  12248  fprodmul  12302  fprodsplitdc  12307  fprodabs  12327  fprod2dlemstep  12333  fproddivapf  12342  eftabs  12367  eftvalcn  12368  efcllemp  12369  ege2le3  12382  efcj  12384  efaddlem  12385  efsep  12402  ef4p  12405  efgt1p2  12406  efgt1p  12407  sinval  12413  cosval  12414  tanvalap  12419  tanval2ap  12424  tanval3ap  12425  efi4p  12428  sinneg  12437  cosneg  12438  tannegap  12439  efival  12443  efmival  12444  sinadd  12447  cosadd  12448  tanaddaplem  12449  tanaddap  12450  sinsub  12451  cossub  12452  addsin  12453  subsin  12454  sinmul  12455  cosmul  12456  addcos  12457  subcos  12458  sincossq  12459  cos2t  12461  sin01bnd  12468  cos01bnd  12469  efieq1re  12483  demoivreALT  12485  dvds2ln  12535  odd2np1lem  12583  bitsinv1lem  12672  gcdaddm  12705  bezoutlemnewy  12717  dfgcd3  12731  dvdsgcd  12733  mulgcd  12737  mulgcdr  12739  gcddiv  12740  sqgcd  12750  lcmgcdlem  12799  lcmgcd  12800  qredeu  12819  divgcdcoprm0  12823  cncongr1  12825  oddpwdclemdc  12895  sqrt2irraplemnn  12901  qnumdenbi  12914  zgcdsq  12923  hashdvds  12943  phiprmpw  12944  phimullem  12947  eulerthlema  12952  prmdiv  12957  modprm0  12977  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  pythagtriplem19  13005  pcval  13019  pcmul  13024  pcdiv  13025  pcqmul  13026  pcid  13047  pcaddlem  13062  pcmpt  13066  pcmpt2  13067  pcmptdvds  13068  pcbc  13074  4sqlem4  13115  mul4sqlem  13116  mul4sq  13117  4sqlem11  13124  4sqlem12  13125  4sqlem15  13128  4sqlem17  13130  ballotfilemfval  13173  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfmpn  13178  ballotfilemgval  13211  ballotfilemgun  13212  ballotfilemfrc  13214  ballotfilemfrceq  13216  ennnfonelemp1  13241  nninfdclemp1  13285  ressvalsets  13361  topnvalg  13548  topnpropgd  13550  qusval  13587  qusex  13589  qusaddvallemg  13597  gsumprval  13662  imasmnd2  13707  ismhm  13716  mhmf1o  13725  0mhm  13741  mhmco  13745  mhmeql  13747  gsumfzz  13750  isgrpid2  13795  grpnpcan  13847  imasgrp2  13863  mhmmnd  13869  mulgnndir  13904  mulgdir  13907  isnsg3  13960  isghm  13996  ghmnsgima  14021  ghmf1o  14028  conjghm  14029  qusghm  14035  ablsub4  14066  ghmcmn  14080  invghm  14082  gsumfzmptfidmadd  14092  gsumfzconst  14094  gsumgfsum  14106  gfsump1  14108  gfsumz  14109  prdsex  14114  prdsval  14115  xpsval  14143  pwsval  14146  mgpvalg  14162  mgptopng  14168  mgpress  14170  rngdi  14179  rngdir  14180  rngpropd  14194  imasrng  14195  srglmhm  14236  srgrmhm  14237  ringo2times  14271  ringcom  14274  ringpropd  14281  ring1  14302  ringlghm  14304  ringrghm  14305  imasring  14307  opprvalg  14312  opprrng  14320  opprring  14322  invrfvald  14367  dvrvald  14379  dvrdir  14388  rdivmuldivd  14389  islmod  14565  lmodlema  14566  islmodd  14567  lmodcom  14607  lmodnegadd  14610  lmodprop2d  14622  rmodislmod  14625  lsssn0  14644  sraval  14711  qusrhm  14802  gsumfzfsumlemm  14861  expghmap  14881  mulgghm2  14882  mulgrhm  14883  zlmval  14901  znval  14910  psrval  14940  mplvalcoe  14971  cnfval  15185  cnpfval  15186  ispsmet  15314  psmet0  15318  psmettri2  15319  psmetres2  15324  ismet  15335  isxmet  15336  xmettri2  15352  xmetres2  15370  xblss2  15396  xmstri2  15461  mstri2  15462  xmstri  15463  mstri  15464  xmstri3  15465  mstri3  15466  msrtri  15467  comet  15490  bdxmet  15492  txmetcnp  15509  metcnpd  15511  cnmet  15521  ioo2bl  15542  mpomulcn  15557  fsumcncntop  15558  elcncf  15564  mulc1cncf  15580  cncfco  15582  cncfcncntop  15584  cncfmptc  15587  cncfmptid  15588  addccncf  15591  cdivcncfap  15595  negcncf  15596  mulcncflem  15598  limccnp2cntop  15668  reldvg  15670  dvfvalap  15672  eldvap  15673  dvconst  15685  dvconstre  15687  dvconstss  15689  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvexp  15702  dvrecap  15704  dvmptid  15707  dvmptc  15708  dveflem  15717  dvef  15718  elplyd  15732  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plyadd  15742  plymul  15743  plycoeid3  15748  plycolemc  15749  plyco  15750  plycjlemc  15751  plycj  15752  plyrecj  15754  dvply1  15756  dvply2g  15757  sinperlem  15799  sinmpi  15806  cosmpi  15807  sinppi  15808  cosppi  15809  efimpi  15810  sinhalfpip  15811  sinhalfpim  15812  coshalfpip  15813  coshalfpim  15814  ptolemy  15815  tangtx  15829  logdivlti  15872  rpcxpadd  15896  rpmulcxp  15900  rplogbchbase  15941  rprelogbmul  15946  binom4  15970  pellexlem2  15972  pellexlem3  15973  wilthlem1  15974  1sgmprm  15988  1sgm2ppw  15989  sgmmul  15990  mersenne  15991  perfect1  15992  perfectlem2  15994  perfect  15995  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsval4a  16021  lgsneg  16023  lgsdilem  16026  lgsdirprm  16033  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  gausslemma2dlem4  16063  gausslemma2dlem6  16066  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  lgsquad2lem2  16081  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2sqlem2  16114  2sqlem3  16116  2sqlem4  16117  2sqlem8  16122  vtxdgfval  16409  vtxdgfifival  16412  vtxdgop  16413  vtxdgfi0e  16416  vtxdeqd  16417  vtxdfifiun  16418  vtxduspgrfvedgfi  16422  1loopgrvd2fi  16426  repiecele0  16936  repiecege0  16937  repiecef  16938  cvgcmp2nlemabs  16942  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trilpo  16953  redcwlpo  16966  nconstwlpolemgt0  16976  nconstwlpo  16978  neapmkv  16980