Theorem oveq12d 5941

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5923

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 5926

This theorem is referenced by:  oveq123d  5944  ovmpodxf  6049  ovmpodf  6055  caovdig  6099  caovdir2d  6101  caovdirg  6102  caovdilemd  6116  caovlem2d  6117  offval  6144  ofvalg  6146  offval2  6152  ofco  6155  caofinvl  6161  offres  6193  nnmsucr  6547  nndir  6549  ecovdi  6706  ecovidi  6707  dfplpq2  7423  dfmpq2  7424  addcmpblnq  7436  mulpipqqs  7442  addassnqg  7451  distrnqg  7456  ltaddnq  7476  halfnqq  7479  enq0tr  7503  addcmpblnq0  7512  addnq0mo  7516  addnnnq0  7518  nqnq0a  7523  distrnq0  7528  addassnq0  7531  distnq0r  7532  nq02m  7534  ltexpri  7682  cauappcvgprlemm  7714  cauappcvgprlemloc  7721  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  cauappcvgprlem1  7728  cauappcvgprlem2  7729  cauappcvgprlemlim  7730  cauappcvgpr  7731  caucvgprlemnkj  7735  caucvgprlemnbj  7736  caucvgprlemm  7737  caucvgprlemloc  7744  caucvgprlemcl  7745  caucvgprlemladdfu  7746  caucvgprlemladdrl  7747  caucvgprlem2  7749  caucvgpr  7751  caucvgprprlemelu  7755  caucvgprprlemcbv  7756  caucvgprprlemval  7757  caucvgprprlemmu  7764  caucvgprprlemopu  7768  caucvgprprlemloc  7772  caucvgprprlemclphr  7774  caucvgprprlemexbt  7775  caucvgprprlem2  7779  mulcmpblnrlemg  7809  mulsrmo  7813  mulsrpr  7815  mulcomsrg  7826  distrsrg  7828  recexgt0sr  7842  mulgt0sr  7847  mulextsr1lem  7849  caucvgsrlemgt1  7864  caucvgsr  7871  addcnsr  7903  mulcnsr  7904  recidpirqlemcalc  7926  axaddcl  7933  axmulcl  7935  axmulcom  7940  axmulass  7942  axdistr  7943  axcaucvglemcau  7967  axcaucvglemres  7968  adddir  8019  muladd11  8161  1p1times  8162  muladd11r  8184  pnpcan2  8268  muladd  8412  subdir  8414  mulsub  8429  mulreim  8633  apadd1  8637  mulext1  8641  recextlem1  8680  muleqadd  8697  divdirap  8726  divadddivap  8756  conjmulap  8758  divcanap5rd  8847  subrecap  8868  xp1d2m1eqxm1d2  9246  div4p1lem1div2  9247  cnref1o  9727  xnegid  9936  xposdif  9959  xleaddadd  9964  icoshftf1o  10068  lincmb01cmp  10080  iccf1o  10081  fz01en  10130  fzrev3  10164  fzrevral2  10183  fzrevral3  10184  fzshftral  10185  fzoaddel2  10271  fzosubel  10272  fzosubel2  10273  fzocatel  10277  modqsubdir  10487  addmodlteq  10492  frecuzrdgsuc  10508  frecfzen2  10521  iseqovex  10552  seqvalcd  10555  seq3caopr3  10585  seqcaopr3g  10586  seq3f1olemqsumkj  10605  seq3f1olemqsumk  10606  seq3f1olemqsum  10607  seqf1oglem2  10614  seq3id3  10618  seqfeq3  10623  seq3distr  10626  ser3le  10631  mulexp  10672  mulexpzap  10673  expaddzap  10677  expubnd  10690  subsq  10740  binom2  10745  binom21  10746  binom2sub  10747  binom2sub1  10748  binom3  10751  sqoddm1div8  10787  mulsubdivbinom2ap  10805  nn0opthlem1d  10814  nn0opthd  10816  facp1  10824  facubnd  10839  bcval  10843  bcn1  10852  bcm1k  10854  bcp1n  10855  bcp1nk  10856  bcval5  10857  bcn2  10858  bcpasc  10860  hashun  10899  hashfz  10915  crre  11024  replim  11026  remullem  11038  remul2  11040  immul2  11047  cjcj  11050  cjadd  11051  ipcnval  11053  cjmulval  11055  cjneg  11057  imval2  11061  cjreim  11070  cvg1nlemcau  11151  cvg1nlemres  11152  resqrexlemp1rp  11173  resqrexlemfp1  11176  resqrexlemcalc1  11181  resqrexlemcalc2  11182  resqrex  11193  sqabsadd  11222  sqabssub  11223  absreimsq  11234  recan  11276  amgm2  11285  maxabslemab  11373  maxabslemval  11375  max0addsup  11386  minabs  11403  bdtrilem  11406  bdtri  11407  xrmaxadd  11428  xrminadd  11442  xrbdtri  11443  subcn2  11478  reccn2ap  11480  climle  11501  climcvg1nlem  11516  serf0  11519  fsumadd  11573  fsumsplit  11574  sumpr  11580  sumtp  11581  isumadd  11598  sumsplitdc  11599  fsum2dlemstep  11601  fsumshftm  11612  fisumrev2  11613  fsumconst  11621  modfsummodlemstep  11624  telfsumo  11633  fsumparts  11637  binomlem  11650  binom  11651  binom1dif  11654  bcxmaslem1  11655  isumsplit  11658  isumnn0nn  11660  arisum  11665  arisum2  11666  trireciplem  11667  trirecip  11668  geosergap  11673  geo2sum  11681  geo2sum2  11682  cvgratnnlemsumlt  11695  mertenslemi1  11702  mertensabs  11704  fprodmul  11758  fprodsplitdc  11763  fprodabs  11783  fprod2dlemstep  11789  fproddivapf  11798  eftabs  11823  eftvalcn  11824  efcllemp  11825  ege2le3  11838  efcj  11840  efaddlem  11841  efsep  11858  ef4p  11861  efgt1p2  11862  efgt1p  11863  sinval  11869  cosval  11870  tanvalap  11875  tanval2ap  11880  tanval3ap  11881  efi4p  11884  sinneg  11893  cosneg  11894  tannegap  11895  efival  11899  efmival  11900  sinadd  11903  cosadd  11904  tanaddaplem  11905  tanaddap  11906  sinsub  11907  cossub  11908  addsin  11909  subsin  11910  sinmul  11911  cosmul  11912  addcos  11913  subcos  11914  sincossq  11915  cos2t  11917  sin01bnd  11924  cos01bnd  11925  efieq1re  11939  demoivreALT  11941  dvds2ln  11991  odd2np1lem  12039  bitsinv1lem  12128  gcdaddm  12161  bezoutlemnewy  12173  dfgcd3  12187  dvdsgcd  12189  mulgcd  12193  mulgcdr  12195  gcddiv  12196  sqgcd  12206  lcmgcdlem  12255  lcmgcd  12256  qredeu  12275  divgcdcoprm0  12279  cncongr1  12281  oddpwdclemdc  12351  sqrt2irraplemnn  12357  qnumdenbi  12370  zgcdsq  12379  hashdvds  12399  phiprmpw  12400  phimullem  12403  eulerthlema  12408  prmdiv  12413  modprm0  12433  coprimeprodsq  12436  pythagtriplem1  12444  pythagtriplem12  12454  pythagtriplem14  12456  pythagtriplem15  12457  pythagtriplem16  12458  pythagtriplem17  12459  pythagtriplem19  12461  pcval  12475  pcmul  12480  pcdiv  12481  pcqmul  12482  pcid  12503  pcaddlem  12518  pcmpt  12522  pcmpt2  12523  pcmptdvds  12524  pcbc  12530  4sqlem4  12571  mul4sqlem  12572  mul4sq  12573  4sqlem11  12580  4sqlem12  12581  4sqlem15  12584  4sqlem17  12586  ennnfonelemp1  12633  nninfdclemp1  12677  ressvalsets  12752  topnvalg  12932  topnpropgd  12934  prdsex  12950  qusval  12976  qusex  12978  qusaddvallemg  12986  xpsval  13005  gsumprval  13052  ismhm  13103  mhmf1o  13112  0mhm  13128  mhmco  13132  mhmeql  13134  gsumfzz  13137  isgrpid2  13182  grpnpcan  13234  imasgrp2  13250  mhmmnd  13256  mulgnndir  13291  mulgdir  13294  isnsg3  13347  isghm  13383  ghmnsgima  13408  ghmf1o  13415  conjghm  13416  qusghm  13422  ablsub4  13453  ghmcmn  13467  invghm  13469  gsumfzmptfidmadd  13479  gsumfzconst  13481  mgpvalg  13489  mgptopng  13495  mgpress  13497  rngdi  13506  rngdir  13507  rngpropd  13521  imasrng  13522  srglmhm  13559  srgrmhm  13560  ringo2times  13594  ringcom  13597  ringpropd  13604  ring1  13625  ringlghm  13627  ringrghm  13628  imasring  13630  opprvalg  13635  opprrng  13643  opprring  13645  invrfvald  13688  dvrvald  13700  dvrdir  13709  rdivmuldivd  13710  islmod  13857  lmodlema  13858  islmodd  13859  lmodcom  13899  lmodnegadd  13902  lmodprop2d  13914  rmodislmod  13917  lsssn0  13936  sraval  14003  qusrhm  14094  gsumfzfsumlemm  14153  expghmap  14173  mulgghm2  14174  mulgrhm  14175  zlmval  14193  znval  14202  psrval  14230  cnfval  14440  cnpfval  14441  ispsmet  14569  psmet0  14573  psmettri2  14574  psmetres2  14579  ismet  14590  isxmet  14591  xmettri2  14607  xmetres2  14625  xblss2  14651  xmstri2  14716  mstri2  14717  xmstri  14718  mstri  14719  xmstri3  14720  mstri3  14721  msrtri  14722  comet  14745  bdxmet  14747  txmetcnp  14764  metcnpd  14766  cnmet  14776  ioo2bl  14797  mpomulcn  14812  fsumcncntop  14813  elcncf  14819  mulc1cncf  14835  cncfco  14837  cncfcncntop  14839  cncfmptc  14842  cncfmptid  14843  addccncf  14846  cdivcncfap  14850  negcncf  14851  mulcncflem  14853  limccnp2cntop  14923  reldvg  14925  dvfvalap  14927  eldvap  14928  dvconst  14940  dvconstre  14942  dvconstss  14944  dvaddxxbr  14947  dvmulxxbr  14948  dvcoapbr  14953  dvcjbr  14954  dvexp  14957  dvrecap  14959  dvmptid  14962  dvmptc  14963  dveflem  14972  dvef  14973  elplyd  14987  ply1termlem  14988  plyaddlem1  14993  plymullem1  14994  plyadd  14997  plymul  14998  plycoeid3  15003  plycolemc  15004  plyco  15005  plycjlemc  15006  plycj  15007  plyrecj  15009  dvply1  15011  dvply2g  15012  sinperlem  15054  sinmpi  15061  cosmpi  15062  sinppi  15063  cosppi  15064  efimpi  15065  sinhalfpip  15066  sinhalfpim  15067  coshalfpip  15068  coshalfpim  15069  ptolemy  15070  tangtx  15084  logdivlti  15127  rpcxpadd  15151  rpmulcxp  15155  rplogbchbase  15196  rprelogbmul  15201  binom4  15225  wilthlem1  15226  1sgmprm  15240  1sgm2ppw  15241  sgmmul  15242  mersenne  15243  perfect1  15244  perfectlem2  15246  perfect  15247  lgsval  15255  lgsfvalg  15256  lgsval2lem  15261  lgsval4a  15273  lgsneg  15275  lgsdilem  15278  lgsdirprm  15285  lgsdir  15286  lgsdilem2  15287  lgsdi  15288  lgsne0  15289  gausslemma2dlem4  15315  gausslemma2dlem6  15318  lgseisenlem2  15322  lgsquadlem1  15328  lgsquadlem2  15329  lgsquadlem3  15330  lgsquad2lem1  15332  lgsquad2lem2  15333  2lgslem3a  15344  2lgslem3b  15345  2lgslem3c  15346  2lgslem3d  15347  2sqlem2  15366  2sqlem3  15368  2sqlem4  15369  2sqlem8  15374  cvgcmp2nlemabs  15686  trilpolemclim  15690  trilpolemcl  15691  trilpolemisumle  15692  trilpolemeq1  15694  trilpolemlt1  15695  trilpo  15697  redcwlpo  15709  nconstwlpolemgt0  15718  nconstwlpo  15720  neapmkv  15722