Theorem oveq12d 5860

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

Syntax hints:   → wi 4   = wceq 1343  (class class class)co 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  oveq123d  5863  ovmpodxf  5967  ovmpodf  5973  caovdig  6016  caovdir2d  6018  caovdirg  6019  caovdilemd  6033  caovlem2d  6034  offval  6057  ofvalg  6059  offval2  6065  ofco  6068  caofinvl  6072  offres  6103  nnmsucr  6456  nndir  6458  ecovdi  6612  ecovidi  6613  dfplpq2  7295  dfmpq2  7296  addcmpblnq  7308  mulpipqqs  7314  addassnqg  7323  distrnqg  7328  ltaddnq  7348  halfnqq  7351  enq0tr  7375  addcmpblnq0  7384  addnq0mo  7388  addnnnq0  7390  nqnq0a  7395  distrnq0  7400  addassnq0  7403  distnq0r  7404  nq02m  7406  ltexpri  7554  cauappcvgprlemm  7586  cauappcvgprlemloc  7593  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlem2  7601  cauappcvgprlemlim  7602  cauappcvgpr  7603  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem2  7621  caucvgpr  7623  caucvgprprlemelu  7627  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemmu  7636  caucvgprprlemopu  7640  caucvgprprlemloc  7644  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  caucvgprprlem2  7651  mulcmpblnrlemg  7681  mulsrmo  7685  mulsrpr  7687  mulcomsrg  7698  distrsrg  7700  recexgt0sr  7714  mulgt0sr  7719  mulextsr1lem  7721  caucvgsrlemgt1  7736  caucvgsr  7743  addcnsr  7775  mulcnsr  7776  recidpirqlemcalc  7798  axaddcl  7805  axmulcl  7807  axmulcom  7812  axmulass  7814  axdistr  7815  axcaucvglemcau  7839  axcaucvglemres  7840  adddir  7890  muladd11  8031  1p1times  8032  muladd11r  8054  pnpcan2  8138  muladd  8282  subdir  8284  mulsub  8299  mulreim  8502  apadd1  8506  mulext1  8510  recextlem1  8548  muleqadd  8565  divdirap  8593  divadddivap  8623  conjmulap  8625  divcanap5rd  8714  subrecap  8735  xp1d2m1eqxm1d2  9109  div4p1lem1div2  9110  cnref1o  9588  xnegid  9795  xposdif  9818  xleaddadd  9823  icoshftf1o  9927  lincmb01cmp  9939  iccf1o  9940  fz01en  9988  fzrev3  10022  fzrevral2  10041  fzrevral3  10042  fzshftral  10043  fzoaddel2  10128  fzosubel  10129  fzosubel2  10130  fzocatel  10134  modqsubdir  10328  addmodlteq  10333  frecuzrdgsuc  10349  frecfzen2  10362  iseqovex  10391  seqvalcd  10394  seq3caopr3  10416  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3id3  10442  seqfeq3  10447  seq3distr  10448  ser3le  10453  mulexp  10494  mulexpzap  10495  expaddzap  10499  expubnd  10512  subsq  10561  binom2  10566  binom21  10567  binom2sub  10568  binom2sub1  10569  binom3  10572  sqoddm1div8  10608  nn0opthlem1d  10633  nn0opthd  10635  facp1  10643  facubnd  10658  bcval  10662  bcn1  10671  bcm1k  10673  bcp1n  10674  bcp1nk  10675  bcval5  10676  bcn2  10677  bcpasc  10679  hashun  10718  hashfz  10734  crre  10799  replim  10801  remullem  10813  remul2  10815  immul2  10822  cjcj  10825  cjadd  10826  ipcnval  10828  cjmulval  10830  cjneg  10832  imval2  10836  cjreim  10845  cvg1nlemcau  10926  cvg1nlemres  10927  resqrexlemp1rp  10948  resqrexlemfp1  10951  resqrexlemcalc1  10956  resqrexlemcalc2  10957  resqrex  10968  sqabsadd  10997  sqabssub  10998  absreimsq  11009  recan  11051  amgm2  11060  maxabslemab  11148  maxabslemval  11150  max0addsup  11161  minabs  11177  bdtrilem  11180  bdtri  11181  xrmaxadd  11202  xrminadd  11216  xrbdtri  11217  subcn2  11252  reccn2ap  11254  climle  11275  climcvg1nlem  11290  serf0  11293  fsumadd  11347  fsumsplit  11348  sumpr  11354  sumtp  11355  isumadd  11372  sumsplitdc  11373  fsum2dlemstep  11375  fsumshftm  11386  fisumrev2  11387  fsumconst  11395  modfsummodlemstep  11398  telfsumo  11407  fsumparts  11411  binomlem  11424  binom  11425  binom1dif  11428  bcxmaslem1  11429  isumsplit  11432  isumnn0nn  11434  arisum  11439  arisum2  11440  trireciplem  11441  trirecip  11442  geosergap  11447  geo2sum  11455  geo2sum2  11456  cvgratnnlemsumlt  11469  mertenslemi1  11476  mertensabs  11478  fprodmul  11532  fprodsplitdc  11537  fprodabs  11557  fprod2dlemstep  11563  fproddivapf  11572  eftabs  11597  eftvalcn  11598  efcllemp  11599  ege2le3  11612  efcj  11614  efaddlem  11615  efsep  11632  ef4p  11635  efgt1p2  11636  efgt1p  11637  sinval  11643  cosval  11644  tanvalap  11649  tanval2ap  11654  tanval3ap  11655  efi4p  11658  sinneg  11667  cosneg  11668  tannegap  11669  efival  11673  efmival  11674  sinadd  11677  cosadd  11678  tanaddaplem  11679  tanaddap  11680  sinsub  11681  cossub  11682  addsin  11683  subsin  11684  sinmul  11685  cosmul  11686  addcos  11687  subcos  11688  sincossq  11689  cos2t  11691  sin01bnd  11698  cos01bnd  11699  efieq1re  11712  demoivreALT  11714  dvds2ln  11764  odd2np1lem  11809  gcdaddm  11917  bezoutlemnewy  11929  dfgcd3  11943  dvdsgcd  11945  mulgcd  11949  mulgcdr  11951  gcddiv  11952  sqgcd  11962  lcmgcdlem  12009  lcmgcd  12010  qredeu  12029  divgcdcoprm0  12033  cncongr1  12035  oddpwdclemdc  12105  sqrt2irraplemnn  12111  qnumdenbi  12124  zgcdsq  12133  hashdvds  12153  phiprmpw  12154  phimullem  12157  eulerthlema  12162  prmdiv  12167  modprm0  12186  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem15  12210  pythagtriplem16  12211  pythagtriplem17  12212  pythagtriplem19  12214  pcval  12228  pcmul  12233  pcdiv  12234  pcqmul  12235  pcid  12255  pcaddlem  12270  pcmpt  12273  pcmpt2  12274  pcmptdvds  12275  pcbc  12281  4sqlem4  12322  mul4sqlem  12323  mul4sq  12324  ennnfonelemp1  12339  nninfdclemp1  12383  ressid2  12454  ressval2  12455  topnvalg  12568  topnpropgd  12570  cnfval  12844  cnpfval  12845  ispsmet  12973  psmet0  12977  psmettri2  12978  psmetres2  12983  ismet  12994  isxmet  12995  xmettri2  13011  xmetres2  13029  xblss2  13055  xmstri2  13120  mstri2  13121  xmstri  13122  mstri  13123  xmstri3  13124  mstri3  13125  msrtri  13126  comet  13149  bdxmet  13151  txmetcnp  13168  metcnpd  13170  cnmet  13180  ioo2bl  13193  fsumcncntop  13206  elcncf  13210  mulc1cncf  13226  cncfco  13228  cncfcncntop  13230  cncfmptc  13232  cncfmptid  13233  addccncf  13236  cdivcncfap  13237  negcncf  13238  mulcncflem  13240  limccnp2cntop  13296  reldvg  13298  dvfvalap  13300  eldvap  13301  dvconst  13311  dvaddxxbr  13315  dvmulxxbr  13316  dvcoapbr  13321  dvcjbr  13322  dvexp  13325  dvrecap  13327  dveflem  13337  dvef  13338  sinperlem  13379  sinmpi  13386  cosmpi  13387  sinppi  13388  cosppi  13389  efimpi  13390  sinhalfpip  13391  sinhalfpim  13392  coshalfpip  13393  coshalfpim  13394  ptolemy  13395  tangtx  13409  logdivlti  13452  rpcxpadd  13476  rpmulcxp  13480  rplogbchbase  13518  rprelogbmul  13523  binom4  13547  lgsval  13555  lgsfvalg  13556  lgsval2lem  13561  lgsval4a  13573  lgsneg  13575  lgsdilem  13578  lgsdirprm  13585  lgsdir  13586  lgsdilem2  13587  lgsdi  13588  lgsne0  13589  2sqlem2  13601  2sqlem3  13603  2sqlem4  13604  2sqlem8  13609  cvgcmp2nlemabs  13921  trilpolemclim  13925  trilpolemcl  13926  trilpolemisumle  13927  trilpolemeq1  13929  trilpolemlt1  13930  trilpo  13932  redcwlpo  13944  nconstwlpolemgt0  13952  nconstwlpo  13954  neapmkv  13956