Theorem oveq12d 6068

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  oveq123d  6071  ovmpodxf  6179  ovmpodf  6185  caovdig  6229  caovdir2d  6231  caovdirg  6232  caovdilemd  6246  caovlem2d  6247  offval  6274  ofvalg  6276  offval2  6282  ofco  6285  caofinvl  6292  offres  6328  nnmsucr  6721  nndir  6723  ecovdi  6880  ecovidi  6881  dfplpq2  7669  dfmpq2  7670  addcmpblnq  7682  mulpipqqs  7688  addassnqg  7697  distrnqg  7702  ltaddnq  7722  halfnqq  7725  enq0tr  7749  addcmpblnq0  7758  addnq0mo  7762  addnnnq0  7764  nqnq0a  7769  distrnq0  7774  addassnq0  7777  distnq0r  7778  nq02m  7780  ltexpri  7928  cauappcvgprlemm  7960  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlem2  7975  cauappcvgprlemlim  7976  cauappcvgpr  7977  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemmu  8010  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem2  8025  mulcmpblnrlemg  8055  mulsrmo  8059  mulsrpr  8061  mulcomsrg  8072  distrsrg  8074  recexgt0sr  8088  mulgt0sr  8093  mulextsr1lem  8095  caucvgsrlemgt1  8110  caucvgsr  8117  addcnsr  8149  mulcnsr  8150  recidpirqlemcalc  8172  axaddcl  8179  axmulcl  8181  axmulcom  8186  axmulass  8188  axdistr  8189  axcaucvglemcau  8213  axcaucvglemres  8214  adddir  8265  muladd11  8406  1p1times  8407  muladd11r  8429  pnpcan2  8513  muladd  8657  subdir  8659  mulsub  8674  mulreim  8878  apadd1  8882  mulext1  8886  recextlem1  8925  muleqadd  8942  divdirap  8971  divadddivap  9001  conjmulap  9003  divcanap5rd  9092  subrecap  9113  xp1d2m1eqxm1d2  9491  div4p1lem1div2  9492  cnref1o  9983  xnegid  10192  xposdif  10215  xleaddadd  10220  icoshftf1o  10324  lincmb01cmp  10336  iccf1o  10338  fz01en  10387  fzrev3  10421  fzrevral2  10440  fzrevral3  10441  fzshftral  10442  fzoaddel2  10535  fzosubel  10539  fzosubel2  10540  fzocatel  10544  modqsubdir  10755  addmodlteq  10760  frecuzrdgsuc  10776  frecfzen2  10789  iseqovex  10820  seqvalcd  10823  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seqf1oglem2  10882  seq3id3  10886  seqfeq3  10891  seq3distr  10894  ser3le  10899  mulexp  10940  mulexpzap  10941  expaddzap  10945  expubnd  10958  subsq  11008  binom2  11013  binom21  11014  binom2sub  11015  binom2sub1  11016  binom3  11019  sqoddm1div8  11055  mulsubdivbinom2ap  11073  nn0opthlem1d  11082  nn0opthd  11084  facp1  11092  facubnd  11107  bcval  11111  bcn1  11120  bcm1k  11122  bcp1n  11123  bcp1nk  11124  bcval5  11125  bcn2  11126  bcpasc  11128  bcm1n  11131  hashun  11169  hashfz  11186  hashfibclem  11206  hashfibc  11207  hashtpgim  11217  ccatlid  11294  ccatass  11296  ccat1st1st  11329  swrdval  11340  swrdspsleq  11359  ccatswrd  11362  pfxval  11366  addlenpfx  11383  ccatpfx  11393  ccatopth  11408  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccat  11427  swrdccat3blem  11431  swrdccatin2d  11436  pfxccatin12d  11437  cats1lend  11459  cats2catd  11461  s2eqd  11462  s3eqd  11463  s4eqd  11464  s5eqd  11465  s6eqd  11466  s7eqd  11467  s8eqd  11468  crre  11542  replim  11544  remullem  11556  remul2  11558  immul2  11565  cjcj  11568  cjadd  11569  ipcnval  11571  cjmulval  11573  cjneg  11575  imval2  11579  cjreim  11588  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemp1rp  11691  resqrexlemfp1  11694  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrex  11711  sqabsadd  11740  sqabssub  11741  absreimsq  11752  recan  11794  amgm2  11803  maxabslemab  11891  maxabslemval  11893  max0addsup  11904  minabs  11921  bdtrilem  11924  bdtri  11925  xrmaxadd  11946  xrminadd  11960  xrbdtri  11961  subcn2  11996  reccn2ap  11998  climle  12019  climcvg1nlem  12034  serf0  12037  fsumadd  12092  fsumsplit  12093  sumpr  12099  sumtp  12100  isumadd  12117  sumsplitdc  12118  fsum2dlemstep  12120  fsumshftm  12131  fisumrev2  12132  fsumconst  12140  modfsummodlemstep  12143  telfsumo  12152  fsumparts  12156  binomlem  12169  binom  12170  binom1dif  12173  bcxmaslem1  12174  isumsplit  12177  isumnn0nn  12179  arisum  12184  arisum2  12185  trireciplem  12186  trirecip  12187  geosergap  12192  geo2sum  12200  geo2sum2  12201  cvgratnnlemsumlt  12214  mertenslemi1  12221  mertensabs  12223  fprodmul  12277  fprodsplitdc  12282  fprodabs  12302  fprod2dlemstep  12308  fproddivapf  12317  eftabs  12342  eftvalcn  12343  efcllemp  12344  ege2le3  12357  efcj  12359  efaddlem  12360  efsep  12377  ef4p  12380  efgt1p2  12381  efgt1p  12382  sinval  12388  cosval  12389  tanvalap  12394  tanval2ap  12399  tanval3ap  12400  efi4p  12403  sinneg  12412  cosneg  12413  tannegap  12414  efival  12418  efmival  12419  sinadd  12422  cosadd  12423  tanaddaplem  12424  tanaddap  12425  sinsub  12426  cossub  12427  addsin  12428  subsin  12429  sinmul  12430  cosmul  12431  addcos  12432  subcos  12433  sincossq  12434  cos2t  12436  sin01bnd  12443  cos01bnd  12444  efieq1re  12458  demoivreALT  12460  dvds2ln  12510  odd2np1lem  12558  bitsinv1lem  12647  gcdaddm  12680  bezoutlemnewy  12692  dfgcd3  12706  dvdsgcd  12708  mulgcd  12712  mulgcdr  12714  gcddiv  12715  sqgcd  12725  lcmgcdlem  12774  lcmgcd  12775  qredeu  12794  divgcdcoprm0  12798  cncongr1  12800  oddpwdclemdc  12870  sqrt2irraplemnn  12876  qnumdenbi  12889  zgcdsq  12898  hashdvds  12918  phiprmpw  12919  phimullem  12922  eulerthlema  12927  prmdiv  12932  modprm0  12952  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  pythagtriplem19  12980  pcval  12994  pcmul  12999  pcdiv  13000  pcqmul  13001  pcid  13022  pcaddlem  13037  pcmpt  13041  pcmpt2  13042  pcmptdvds  13043  pcbc  13049  4sqlem4  13090  mul4sqlem  13091  mul4sq  13092  4sqlem11  13099  4sqlem12  13100  4sqlem15  13103  4sqlem17  13105  ennnfonelemp1  13157  nninfdclemp1  13201  ressvalsets  13277  topnvalg  13464  topnpropgd  13466  prdsex  13482  prdsval  13486  pwsval  13504  qusval  13536  qusex  13538  qusaddvallemg  13546  xpsval  13565  gsumprval  13612  imasmnd2  13665  ismhm  13674  mhmf1o  13683  0mhm  13699  mhmco  13703  mhmeql  13705  gsumfzz  13708  isgrpid2  13753  grpnpcan  13805  imasgrp2  13827  mhmmnd  13833  mulgnndir  13868  mulgdir  13871  isnsg3  13924  isghm  13960  ghmnsgima  13985  ghmf1o  13992  conjghm  13993  qusghm  13999  ablsub4  14030  ghmcmn  14044  invghm  14046  gsumfzmptfidmadd  14056  gsumfzconst  14058  mgpvalg  14067  mgptopng  14073  mgpress  14075  rngdi  14084  rngdir  14085  rngpropd  14099  imasrng  14100  srglmhm  14137  srgrmhm  14138  ringo2times  14172  ringcom  14175  ringpropd  14182  ring1  14203  ringlghm  14205  ringrghm  14206  imasring  14208  opprvalg  14213  opprrng  14221  opprring  14223  invrfvald  14267  dvrvald  14279  dvrdir  14288  rdivmuldivd  14289  islmod  14439  lmodlema  14440  islmodd  14441  lmodcom  14481  lmodnegadd  14484  lmodprop2d  14496  rmodislmod  14499  lsssn0  14518  sraval  14585  qusrhm  14676  gsumfzfsumlemm  14735  expghmap  14755  mulgghm2  14756  mulgrhm  14757  zlmval  14775  znval  14784  psrval  14814  mplvalcoe  14845  cnfval  15059  cnpfval  15060  ispsmet  15188  psmet0  15192  psmettri2  15193  psmetres2  15198  ismet  15209  isxmet  15210  xmettri2  15226  xmetres2  15244  xblss2  15270  xmstri2  15335  mstri2  15336  xmstri  15337  mstri  15338  xmstri3  15339  mstri3  15340  msrtri  15341  comet  15364  bdxmet  15366  txmetcnp  15383  metcnpd  15385  cnmet  15395  ioo2bl  15416  mpomulcn  15431  fsumcncntop  15432  elcncf  15438  mulc1cncf  15454  cncfco  15456  cncfcncntop  15458  cncfmptc  15461  cncfmptid  15462  addccncf  15465  cdivcncfap  15469  negcncf  15470  mulcncflem  15472  limccnp2cntop  15542  reldvg  15544  dvfvalap  15546  eldvap  15547  dvconst  15559  dvconstre  15561  dvconstss  15563  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvexp  15576  dvrecap  15578  dvmptid  15581  dvmptc  15582  dveflem  15591  dvef  15592  elplyd  15606  ply1termlem  15607  plyaddlem1  15612  plymullem1  15613  plyadd  15616  plymul  15617  plycoeid3  15622  plycolemc  15623  plyco  15624  plycjlemc  15625  plycj  15626  plyrecj  15628  dvply1  15630  dvply2g  15631  sinperlem  15673  sinmpi  15680  cosmpi  15681  sinppi  15682  cosppi  15683  efimpi  15684  sinhalfpip  15685  sinhalfpim  15686  coshalfpip  15687  coshalfpim  15688  ptolemy  15689  tangtx  15703  logdivlti  15746  rpcxpadd  15770  rpmulcxp  15774  rplogbchbase  15815  rprelogbmul  15820  binom4  15844  pellexlem2  15846  pellexlem3  15847  wilthlem1  15848  1sgmprm  15862  1sgm2ppw  15863  sgmmul  15864  mersenne  15865  perfect1  15866  perfectlem2  15868  perfect  15869  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsdilem  15900  lgsdirprm  15907  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  gausslemma2dlem4  15937  gausslemma2dlem6  15940  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad2lem2  15955  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2sqlem2  15988  2sqlem3  15990  2sqlem4  15991  2sqlem8  15996  vtxdgfval  16283  vtxdgfifival  16286  vtxdgop  16287  vtxdgfi0e  16290  vtxdeqd  16291  vtxdfifiun  16292  vtxduspgrfvedgfi  16296  1loopgrvd2fi  16300  repiecele0  16810  repiecege0  16811  repiecef  16812  cvgcmp2nlemabs  16816  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trilpo  16827  redcwlpo  16840  nconstwlpolemgt0  16850  nconstwlpo  16852  neapmkv  16854  gsumgfsum  16866  gfsump1  16868  gfsumz  16869