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  7440  dfmpq2  7441  addcmpblnq  7453  mulpipqqs  7459  addassnqg  7468  distrnqg  7473  ltaddnq  7493  halfnqq  7496  enq0tr  7520  addcmpblnq0  7529  addnq0mo  7533  addnnnq0  7535  nqnq0a  7540  distrnq0  7545  addassnq0  7548  distnq0r  7549  nq02m  7551  ltexpri  7699  cauappcvgprlemm  7731  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemmu  7781  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexbt  7792  caucvgprprlem2  7796  mulcmpblnrlemg  7826  mulsrmo  7830  mulsrpr  7832  mulcomsrg  7843  distrsrg  7845  recexgt0sr  7859  mulgt0sr  7864  mulextsr1lem  7866  caucvgsrlemgt1  7881  caucvgsr  7888  addcnsr  7920  mulcnsr  7921  recidpirqlemcalc  7943  axaddcl  7950  axmulcl  7952  axmulcom  7957  axmulass  7959  axdistr  7960  axcaucvglemcau  7984  axcaucvglemres  7985  adddir  8036  muladd11  8178  1p1times  8179  muladd11r  8201  pnpcan2  8285  muladd  8429  subdir  8431  mulsub  8446  mulreim  8650  apadd1  8654  mulext1  8658  recextlem1  8697  muleqadd  8714  divdirap  8743  divadddivap  8773  conjmulap  8775  divcanap5rd  8864  subrecap  8885  xp1d2m1eqxm1d2  9263  div4p1lem1div2  9264  cnref1o  9744  xnegid  9953  xposdif  9976  xleaddadd  9981  icoshftf1o  10085  lincmb01cmp  10097  iccf1o  10098  fz01en  10147  fzrev3  10181  fzrevral2  10200  fzrevral3  10201  fzshftral  10202  fzoaddel2  10288  fzosubel  10289  fzosubel2  10290  fzocatel  10294  modqsubdir  10504  addmodlteq  10509  frecuzrdgsuc  10525  frecfzen2  10538  iseqovex  10569  seqvalcd  10572  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seqf1oglem2  10631  seq3id3  10635  seqfeq3  10640  seq3distr  10643  ser3le  10648  mulexp  10689  mulexpzap  10690  expaddzap  10694  expubnd  10707  subsq  10757  binom2  10762  binom21  10763  binom2sub  10764  binom2sub1  10765  binom3  10768  sqoddm1div8  10804  mulsubdivbinom2ap  10822  nn0opthlem1d  10831  nn0opthd  10833  facp1  10841  facubnd  10856  bcval  10860  bcn1  10869  bcm1k  10871  bcp1n  10872  bcp1nk  10873  bcval5  10874  bcn2  10875  bcpasc  10877  hashun  10916  hashfz  10932  crre  11041  replim  11043  remullem  11055  remul2  11057  immul2  11064  cjcj  11067  cjadd  11068  ipcnval  11070  cjmulval  11072  cjneg  11074  imval2  11078  cjreim  11087  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemp1rp  11190  resqrexlemfp1  11193  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrex  11210  sqabsadd  11239  sqabssub  11240  absreimsq  11251  recan  11293  amgm2  11302  maxabslemab  11390  maxabslemval  11392  max0addsup  11403  minabs  11420  bdtrilem  11423  bdtri  11424  xrmaxadd  11445  xrminadd  11459  xrbdtri  11460  subcn2  11495  reccn2ap  11497  climle  11518  climcvg1nlem  11533  serf0  11536  fsumadd  11590  fsumsplit  11591  sumpr  11597  sumtp  11598  isumadd  11615  sumsplitdc  11616  fsum2dlemstep  11618  fsumshftm  11629  fisumrev2  11630  fsumconst  11638  modfsummodlemstep  11641  telfsumo  11650  fsumparts  11654  binomlem  11667  binom  11668  binom1dif  11671  bcxmaslem1  11672  isumsplit  11675  isumnn0nn  11677  arisum  11682  arisum2  11683  trireciplem  11684  trirecip  11685  geosergap  11690  geo2sum  11698  geo2sum2  11699  cvgratnnlemsumlt  11712  mertenslemi1  11719  mertensabs  11721  fprodmul  11775  fprodsplitdc  11780  fprodabs  11800  fprod2dlemstep  11806  fproddivapf  11815  eftabs  11840  eftvalcn  11841  efcllemp  11842  ege2le3  11855  efcj  11857  efaddlem  11858  efsep  11875  ef4p  11878  efgt1p2  11879  efgt1p  11880  sinval  11886  cosval  11887  tanvalap  11892  tanval2ap  11897  tanval3ap  11898  efi4p  11901  sinneg  11910  cosneg  11911  tannegap  11912  efival  11916  efmival  11917  sinadd  11920  cosadd  11921  tanaddaplem  11922  tanaddap  11923  sinsub  11924  cossub  11925  addsin  11926  subsin  11927  sinmul  11928  cosmul  11929  addcos  11930  subcos  11931  sincossq  11932  cos2t  11934  sin01bnd  11941  cos01bnd  11942  efieq1re  11956  demoivreALT  11958  dvds2ln  12008  odd2np1lem  12056  bitsinv1lem  12145  gcdaddm  12178  bezoutlemnewy  12190  dfgcd3  12204  dvdsgcd  12206  mulgcd  12210  mulgcdr  12212  gcddiv  12213  sqgcd  12223  lcmgcdlem  12272  lcmgcd  12273  qredeu  12292  divgcdcoprm0  12296  cncongr1  12298  oddpwdclemdc  12368  sqrt2irraplemnn  12374  qnumdenbi  12387  zgcdsq  12396  hashdvds  12416  phiprmpw  12417  phimullem  12420  eulerthlema  12425  prmdiv  12430  modprm0  12450  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  pythagtriplem19  12478  pcval  12492  pcmul  12497  pcdiv  12498  pcqmul  12499  pcid  12520  pcaddlem  12535  pcmpt  12539  pcmpt2  12540  pcmptdvds  12541  pcbc  12547  4sqlem4  12588  mul4sqlem  12589  mul4sq  12590  4sqlem11  12597  4sqlem12  12598  4sqlem15  12601  4sqlem17  12603  ennnfonelemp1  12650  nninfdclemp1  12694  ressvalsets  12769  topnvalg  12955  topnpropgd  12957  prdsex  12973  prdsval  12977  pwsval  12995  qusval  13027  qusex  13029  qusaddvallemg  13037  xpsval  13056  gsumprval  13103  imasmnd2  13156  ismhm  13165  mhmf1o  13174  0mhm  13190  mhmco  13194  mhmeql  13196  gsumfzz  13199  isgrpid2  13244  grpnpcan  13296  imasgrp2  13318  mhmmnd  13324  mulgnndir  13359  mulgdir  13362  isnsg3  13415  isghm  13451  ghmnsgima  13476  ghmf1o  13483  conjghm  13484  qusghm  13490  ablsub4  13521  ghmcmn  13535  invghm  13537  gsumfzmptfidmadd  13547  gsumfzconst  13549  mgpvalg  13557  mgptopng  13563  mgpress  13565  rngdi  13574  rngdir  13575  rngpropd  13589  imasrng  13590  srglmhm  13627  srgrmhm  13628  ringo2times  13662  ringcom  13665  ringpropd  13672  ring1  13693  ringlghm  13695  ringrghm  13696  imasring  13698  opprvalg  13703  opprrng  13711  opprring  13713  invrfvald  13756  dvrvald  13768  dvrdir  13777  rdivmuldivd  13778  islmod  13925  lmodlema  13926  islmodd  13927  lmodcom  13967  lmodnegadd  13970  lmodprop2d  13982  rmodislmod  13985  lsssn0  14004  sraval  14071  qusrhm  14162  gsumfzfsumlemm  14221  expghmap  14241  mulgghm2  14242  mulgrhm  14243  zlmval  14261  znval  14270  psrval  14300  mplvalcoe  14324  cnfval  14538  cnpfval  14539  ispsmet  14667  psmet0  14671  psmettri2  14672  psmetres2  14677  ismet  14688  isxmet  14689  xmettri2  14705  xmetres2  14723  xblss2  14749  xmstri2  14814  mstri2  14815  xmstri  14816  mstri  14817  xmstri3  14818  mstri3  14819  msrtri  14820  comet  14843  bdxmet  14845  txmetcnp  14862  metcnpd  14864  cnmet  14874  ioo2bl  14895  mpomulcn  14910  fsumcncntop  14911  elcncf  14917  mulc1cncf  14933  cncfco  14935  cncfcncntop  14937  cncfmptc  14940  cncfmptid  14941  addccncf  14944  cdivcncfap  14948  negcncf  14949  mulcncflem  14951  limccnp2cntop  15021  reldvg  15023  dvfvalap  15025  eldvap  15026  dvconst  15038  dvconstre  15040  dvconstss  15042  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvexp  15055  dvrecap  15057  dvmptid  15060  dvmptc  15061  dveflem  15070  dvef  15071  elplyd  15085  ply1termlem  15086  plyaddlem1  15091  plymullem1  15092  plyadd  15095  plymul  15096  plycoeid3  15101  plycolemc  15102  plyco  15103  plycjlemc  15104  plycj  15105  plyrecj  15107  dvply1  15109  dvply2g  15110  sinperlem  15152  sinmpi  15159  cosmpi  15160  sinppi  15161  cosppi  15162  efimpi  15163  sinhalfpip  15164  sinhalfpim  15165  coshalfpip  15166  coshalfpim  15167  ptolemy  15168  tangtx  15182  logdivlti  15225  rpcxpadd  15249  rpmulcxp  15253  rplogbchbase  15294  rprelogbmul  15299  binom4  15323  wilthlem1  15324  1sgmprm  15338  1sgm2ppw  15339  sgmmul  15340  mersenne  15341  perfect1  15342  perfectlem2  15344  perfect  15345  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsval4a  15371  lgsneg  15373  lgsdilem  15376  lgsdirprm  15383  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  gausslemma2dlem4  15413  gausslemma2dlem6  15416  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  lgsquad2lem2  15431  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2sqlem2  15464  2sqlem3  15466  2sqlem4  15467  2sqlem8  15472  cvgcmp2nlemabs  15789  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trilpo  15800  redcwlpo  15812  nconstwlpolemgt0  15821  nconstwlpo  15823  neapmkv  15825