Theorem oveq12d 6035

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

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveq123d  6038  ovmpodxf  6146  ovmpodf  6152  caovdig  6196  caovdir2d  6198  caovdirg  6199  caovdilemd  6213  caovlem2d  6214  offval  6242  ofvalg  6244  offval2  6250  ofco  6253  caofinvl  6260  offres  6296  nnmsucr  6655  nndir  6657  ecovdi  6814  ecovidi  6815  dfplpq2  7573  dfmpq2  7574  addcmpblnq  7586  mulpipqqs  7592  addassnqg  7601  distrnqg  7606  ltaddnq  7626  halfnqq  7629  enq0tr  7653  addcmpblnq0  7662  addnq0mo  7666  addnnnq0  7668  nqnq0a  7673  distrnq0  7678  addassnq0  7681  distnq0r  7682  nq02m  7684  ltexpri  7832  cauappcvgprlemm  7864  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  cauappcvgprlemlim  7880  cauappcvgpr  7881  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemmu  7914  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem2  7929  mulcmpblnrlemg  7959  mulsrmo  7963  mulsrpr  7965  mulcomsrg  7976  distrsrg  7978  recexgt0sr  7992  mulgt0sr  7997  mulextsr1lem  7999  caucvgsrlemgt1  8014  caucvgsr  8021  addcnsr  8053  mulcnsr  8054  recidpirqlemcalc  8076  axaddcl  8083  axmulcl  8085  axmulcom  8090  axmulass  8092  axdistr  8093  axcaucvglemcau  8117  axcaucvglemres  8118  adddir  8169  muladd11  8311  1p1times  8312  muladd11r  8334  pnpcan2  8418  muladd  8562  subdir  8564  mulsub  8579  mulreim  8783  apadd1  8787  mulext1  8791  recextlem1  8830  muleqadd  8847  divdirap  8876  divadddivap  8906  conjmulap  8908  divcanap5rd  8997  subrecap  9018  xp1d2m1eqxm1d2  9396  div4p1lem1div2  9397  cnref1o  9884  xnegid  10093  xposdif  10116  xleaddadd  10121  icoshftf1o  10225  lincmb01cmp  10237  iccf1o  10238  fz01en  10287  fzrev3  10321  fzrevral2  10340  fzrevral3  10341  fzshftral  10342  fzoaddel2  10434  fzosubel  10438  fzosubel2  10439  fzocatel  10443  modqsubdir  10654  addmodlteq  10659  frecuzrdgsuc  10675  frecfzen2  10688  iseqovex  10719  seqvalcd  10722  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seqf1oglem2  10781  seq3id3  10785  seqfeq3  10790  seq3distr  10793  ser3le  10798  mulexp  10839  mulexpzap  10840  expaddzap  10844  expubnd  10857  subsq  10907  binom2  10912  binom21  10913  binom2sub  10914  binom2sub1  10915  binom3  10918  sqoddm1div8  10954  mulsubdivbinom2ap  10972  nn0opthlem1d  10981  nn0opthd  10983  facp1  10991  facubnd  11006  bcval  11010  bcn1  11019  bcm1k  11021  bcp1n  11022  bcp1nk  11023  bcval5  11024  bcn2  11025  bcpasc  11027  hashun  11067  hashfz  11084  ccatlid  11182  ccatass  11184  ccat1st1st  11217  swrdval  11228  swrdspsleq  11247  ccatswrd  11250  pfxval  11254  addlenpfx  11271  ccatpfx  11281  ccatopth  11296  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccat  11315  swrdccat3blem  11319  swrdccatin2d  11324  pfxccatin12d  11325  cats1lend  11347  cats2catd  11349  s2eqd  11350  s3eqd  11351  s4eqd  11352  s5eqd  11353  s6eqd  11354  s7eqd  11355  s8eqd  11356  crre  11417  replim  11419  remullem  11431  remul2  11433  immul2  11440  cjcj  11443  cjadd  11444  ipcnval  11446  cjmulval  11448  cjneg  11450  imval2  11454  cjreim  11463  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrex  11586  sqabsadd  11615  sqabssub  11616  absreimsq  11627  recan  11669  amgm2  11678  maxabslemab  11766  maxabslemval  11768  max0addsup  11779  minabs  11796  bdtrilem  11799  bdtri  11800  xrmaxadd  11821  xrminadd  11835  xrbdtri  11836  subcn2  11871  reccn2ap  11873  climle  11894  climcvg1nlem  11909  serf0  11912  fsumadd  11966  fsumsplit  11967  sumpr  11973  sumtp  11974  isumadd  11991  sumsplitdc  11992  fsum2dlemstep  11994  fsumshftm  12005  fisumrev2  12006  fsumconst  12014  modfsummodlemstep  12017  telfsumo  12026  fsumparts  12030  binomlem  12043  binom  12044  binom1dif  12047  bcxmaslem1  12048  isumsplit  12051  isumnn0nn  12053  arisum  12058  arisum2  12059  trireciplem  12060  trirecip  12061  geosergap  12066  geo2sum  12074  geo2sum2  12075  cvgratnnlemsumlt  12088  mertenslemi1  12095  mertensabs  12097  fprodmul  12151  fprodsplitdc  12156  fprodabs  12176  fprod2dlemstep  12182  fproddivapf  12191  eftabs  12216  eftvalcn  12217  efcllemp  12218  ege2le3  12231  efcj  12233  efaddlem  12234  efsep  12251  ef4p  12254  efgt1p2  12255  efgt1p  12256  sinval  12262  cosval  12263  tanvalap  12268  tanval2ap  12273  tanval3ap  12274  efi4p  12277  sinneg  12286  cosneg  12287  tannegap  12288  efival  12292  efmival  12293  sinadd  12296  cosadd  12297  tanaddaplem  12298  tanaddap  12299  sinsub  12300  cossub  12301  addsin  12302  subsin  12303  sinmul  12304  cosmul  12305  addcos  12306  subcos  12307  sincossq  12308  cos2t  12310  sin01bnd  12317  cos01bnd  12318  efieq1re  12332  demoivreALT  12334  dvds2ln  12384  odd2np1lem  12432  bitsinv1lem  12521  gcdaddm  12554  bezoutlemnewy  12566  dfgcd3  12580  dvdsgcd  12582  mulgcd  12586  mulgcdr  12588  gcddiv  12589  sqgcd  12599  lcmgcdlem  12648  lcmgcd  12649  qredeu  12668  divgcdcoprm0  12672  cncongr1  12674  oddpwdclemdc  12744  sqrt2irraplemnn  12750  qnumdenbi  12763  zgcdsq  12772  hashdvds  12792  phiprmpw  12793  phimullem  12796  eulerthlema  12801  prmdiv  12806  modprm0  12826  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  pythagtriplem19  12854  pcval  12868  pcmul  12873  pcdiv  12874  pcqmul  12875  pcid  12896  pcaddlem  12911  pcmpt  12915  pcmpt2  12916  pcmptdvds  12917  pcbc  12923  4sqlem4  12964  mul4sqlem  12965  mul4sq  12966  4sqlem11  12973  4sqlem12  12974  4sqlem15  12977  4sqlem17  12979  ennnfonelemp1  13026  nninfdclemp1  13070  ressvalsets  13146  topnvalg  13333  topnpropgd  13335  prdsex  13351  prdsval  13355  pwsval  13373  qusval  13405  qusex  13407  qusaddvallemg  13415  xpsval  13434  gsumprval  13481  imasmnd2  13534  ismhm  13543  mhmf1o  13552  0mhm  13568  mhmco  13572  mhmeql  13574  gsumfzz  13577  isgrpid2  13622  grpnpcan  13674  imasgrp2  13696  mhmmnd  13702  mulgnndir  13737  mulgdir  13740  isnsg3  13793  isghm  13829  ghmnsgima  13854  ghmf1o  13861  conjghm  13862  qusghm  13868  ablsub4  13899  ghmcmn  13913  invghm  13915  gsumfzmptfidmadd  13925  gsumfzconst  13927  mgpvalg  13935  mgptopng  13941  mgpress  13943  rngdi  13952  rngdir  13953  rngpropd  13967  imasrng  13968  srglmhm  14005  srgrmhm  14006  ringo2times  14040  ringcom  14043  ringpropd  14050  ring1  14071  ringlghm  14073  ringrghm  14074  imasring  14076  opprvalg  14081  opprrng  14089  opprring  14091  invrfvald  14135  dvrvald  14147  dvrdir  14156  rdivmuldivd  14157  islmod  14304  lmodlema  14305  islmodd  14306  lmodcom  14346  lmodnegadd  14349  lmodprop2d  14361  rmodislmod  14364  lsssn0  14383  sraval  14450  qusrhm  14541  gsumfzfsumlemm  14600  expghmap  14620  mulgghm2  14621  mulgrhm  14622  zlmval  14640  znval  14649  psrval  14679  mplvalcoe  14703  cnfval  14917  cnpfval  14918  ispsmet  15046  psmet0  15050  psmettri2  15051  psmetres2  15056  ismet  15067  isxmet  15068  xmettri2  15084  xmetres2  15102  xblss2  15128  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  comet  15222  bdxmet  15224  txmetcnp  15241  metcnpd  15243  cnmet  15253  ioo2bl  15274  mpomulcn  15289  fsumcncntop  15290  elcncf  15296  mulc1cncf  15312  cncfco  15314  cncfcncntop  15316  cncfmptc  15319  cncfmptid  15320  addccncf  15323  cdivcncfap  15327  negcncf  15328  mulcncflem  15330  limccnp2cntop  15400  reldvg  15402  dvfvalap  15404  eldvap  15405  dvconst  15417  dvconstre  15419  dvconstss  15421  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvexp  15434  dvrecap  15436  dvmptid  15439  dvmptc  15440  dveflem  15449  dvef  15450  elplyd  15464  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plyadd  15474  plymul  15475  plycoeid3  15480  plycolemc  15481  plyco  15482  plycjlemc  15483  plycj  15484  plyrecj  15486  dvply1  15488  dvply2g  15489  sinperlem  15531  sinmpi  15538  cosmpi  15539  sinppi  15540  cosppi  15541  efimpi  15542  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  ptolemy  15547  tangtx  15561  logdivlti  15604  rpcxpadd  15628  rpmulcxp  15632  rplogbchbase  15673  rprelogbmul  15678  binom4  15702  wilthlem1  15703  1sgmprm  15717  1sgm2ppw  15718  sgmmul  15719  mersenne  15720  perfect1  15721  perfectlem2  15723  perfect  15724  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsval4a  15750  lgsneg  15752  lgsdilem  15755  lgsdirprm  15762  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  gausslemma2dlem4  15792  gausslemma2dlem6  15795  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  lgsquad2lem2  15810  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2sqlem2  15843  2sqlem3  15845  2sqlem4  15846  2sqlem8  15851  vtxdgfval  16138  vtxdgfifival  16141  vtxdgop  16142  vtxdgfi0e  16145  vtxdeqd  16146  vtxdfifiun  16147  vtxduspgrfvedgfi  16151  1loopgrvd2fi  16155  cvgcmp2nlemabs  16636  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trilpo  16647  redcwlpo  16659  nconstwlpolemgt0  16668  nconstwlpo  16670  neapmkv  16672  gsumgfsum  16684