Theorem oveq12d 5936

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  oveq123d  5939  ovmpodxf  6044  ovmpodf  6050  caovdig  6093  caovdir2d  6095  caovdirg  6096  caovdilemd  6110  caovlem2d  6111  offval  6138  ofvalg  6140  offval2  6146  ofco  6149  caofinvl  6155  offres  6187  nnmsucr  6541  nndir  6543  ecovdi  6700  ecovidi  6701  dfplpq2  7414  dfmpq2  7415  addcmpblnq  7427  mulpipqqs  7433  addassnqg  7442  distrnqg  7447  ltaddnq  7467  halfnqq  7470  enq0tr  7494  addcmpblnq0  7503  addnq0mo  7507  addnnnq0  7509  nqnq0a  7514  distrnq0  7519  addassnq0  7522  distnq0r  7523  nq02m  7525  ltexpri  7673  cauappcvgprlemm  7705  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  cauappcvgprlemlim  7721  cauappcvgpr  7722  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemmu  7755  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem2  7770  mulcmpblnrlemg  7800  mulsrmo  7804  mulsrpr  7806  mulcomsrg  7817  distrsrg  7819  recexgt0sr  7833  mulgt0sr  7838  mulextsr1lem  7840  caucvgsrlemgt1  7855  caucvgsr  7862  addcnsr  7894  mulcnsr  7895  recidpirqlemcalc  7917  axaddcl  7924  axmulcl  7926  axmulcom  7931  axmulass  7933  axdistr  7934  axcaucvglemcau  7958  axcaucvglemres  7959  adddir  8010  muladd11  8152  1p1times  8153  muladd11r  8175  pnpcan2  8259  muladd  8403  subdir  8405  mulsub  8420  mulreim  8623  apadd1  8627  mulext1  8631  recextlem1  8670  muleqadd  8687  divdirap  8716  divadddivap  8746  conjmulap  8748  divcanap5rd  8837  subrecap  8858  xp1d2m1eqxm1d2  9235  div4p1lem1div2  9236  cnref1o  9716  xnegid  9925  xposdif  9948  xleaddadd  9953  icoshftf1o  10057  lincmb01cmp  10069  iccf1o  10070  fz01en  10119  fzrev3  10153  fzrevral2  10172  fzrevral3  10173  fzshftral  10174  fzoaddel2  10260  fzosubel  10261  fzosubel2  10262  fzocatel  10266  modqsubdir  10464  addmodlteq  10469  frecuzrdgsuc  10485  frecfzen2  10498  iseqovex  10529  seqvalcd  10532  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seqf1oglem2  10591  seq3id3  10595  seqfeq3  10600  seq3distr  10603  ser3le  10608  mulexp  10649  mulexpzap  10650  expaddzap  10654  expubnd  10667  subsq  10717  binom2  10722  binom21  10723  binom2sub  10724  binom2sub1  10725  binom3  10728  sqoddm1div8  10764  mulsubdivbinom2ap  10782  nn0opthlem1d  10791  nn0opthd  10793  facp1  10801  facubnd  10816  bcval  10820  bcn1  10829  bcm1k  10831  bcp1n  10832  bcp1nk  10833  bcval5  10834  bcn2  10835  bcpasc  10837  hashun  10876  hashfz  10892  crre  11001  replim  11003  remullem  11015  remul2  11017  immul2  11024  cjcj  11027  cjadd  11028  ipcnval  11030  cjmulval  11032  cjneg  11034  imval2  11038  cjreim  11047  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemp1rp  11150  resqrexlemfp1  11153  resqrexlemcalc1  11158  resqrexlemcalc2  11159  resqrex  11170  sqabsadd  11199  sqabssub  11200  absreimsq  11211  recan  11253  amgm2  11262  maxabslemab  11350  maxabslemval  11352  max0addsup  11363  minabs  11379  bdtrilem  11382  bdtri  11383  xrmaxadd  11404  xrminadd  11418  xrbdtri  11419  subcn2  11454  reccn2ap  11456  climle  11477  climcvg1nlem  11492  serf0  11495  fsumadd  11549  fsumsplit  11550  sumpr  11556  sumtp  11557  isumadd  11574  sumsplitdc  11575  fsum2dlemstep  11577  fsumshftm  11588  fisumrev2  11589  fsumconst  11597  modfsummodlemstep  11600  telfsumo  11609  fsumparts  11613  binomlem  11626  binom  11627  binom1dif  11630  bcxmaslem1  11631  isumsplit  11634  isumnn0nn  11636  arisum  11641  arisum2  11642  trireciplem  11643  trirecip  11644  geosergap  11649  geo2sum  11657  geo2sum2  11658  cvgratnnlemsumlt  11671  mertenslemi1  11678  mertensabs  11680  fprodmul  11734  fprodsplitdc  11739  fprodabs  11759  fprod2dlemstep  11765  fproddivapf  11774  eftabs  11799  eftvalcn  11800  efcllemp  11801  ege2le3  11814  efcj  11816  efaddlem  11817  efsep  11834  ef4p  11837  efgt1p2  11838  efgt1p  11839  sinval  11845  cosval  11846  tanvalap  11851  tanval2ap  11856  tanval3ap  11857  efi4p  11860  sinneg  11869  cosneg  11870  tannegap  11871  efival  11875  efmival  11876  sinadd  11879  cosadd  11880  tanaddaplem  11881  tanaddap  11882  sinsub  11883  cossub  11884  addsin  11885  subsin  11886  sinmul  11887  cosmul  11888  addcos  11889  subcos  11890  sincossq  11891  cos2t  11893  sin01bnd  11900  cos01bnd  11901  efieq1re  11915  demoivreALT  11917  dvds2ln  11967  odd2np1lem  12013  gcdaddm  12121  bezoutlemnewy  12133  dfgcd3  12147  dvdsgcd  12149  mulgcd  12153  mulgcdr  12155  gcddiv  12156  sqgcd  12166  lcmgcdlem  12215  lcmgcd  12216  qredeu  12235  divgcdcoprm0  12239  cncongr1  12241  oddpwdclemdc  12311  sqrt2irraplemnn  12317  qnumdenbi  12330  zgcdsq  12339  hashdvds  12359  phiprmpw  12360  phimullem  12363  eulerthlema  12368  prmdiv  12373  modprm0  12392  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  pythagtriplem19  12420  pcval  12434  pcmul  12439  pcdiv  12440  pcqmul  12441  pcid  12462  pcaddlem  12477  pcmpt  12481  pcmpt2  12482  pcmptdvds  12483  pcbc  12489  4sqlem4  12530  mul4sqlem  12531  mul4sq  12532  4sqlem11  12539  4sqlem12  12540  4sqlem15  12543  4sqlem17  12545  ennnfonelemp1  12563  nninfdclemp1  12607  ressvalsets  12682  topnvalg  12862  topnpropgd  12864  prdsex  12880  qusval  12906  qusex  12908  qusaddvallemg  12916  xpsval  12935  gsumprval  12982  ismhm  13033  mhmf1o  13042  0mhm  13058  mhmco  13062  mhmeql  13064  gsumfzz  13067  isgrpid2  13112  grpnpcan  13164  imasgrp2  13180  mhmmnd  13186  mulgnndir  13221  mulgdir  13224  isnsg3  13277  isghm  13313  ghmnsgima  13338  ghmf1o  13345  conjghm  13346  qusghm  13352  ablsub4  13383  ghmcmn  13397  invghm  13399  gsumfzmptfidmadd  13409  gsumfzconst  13411  mgpvalg  13419  mgptopng  13425  mgpress  13427  rngdi  13436  rngdir  13437  rngpropd  13451  imasrng  13452  srglmhm  13489  srgrmhm  13490  ringo2times  13524  ringcom  13527  ringpropd  13534  ring1  13555  ringlghm  13557  ringrghm  13558  imasring  13560  opprvalg  13565  opprrng  13573  opprring  13575  invrfvald  13618  dvrvald  13630  dvrdir  13639  rdivmuldivd  13640  islmod  13787  lmodlema  13788  islmodd  13789  lmodcom  13829  lmodnegadd  13832  lmodprop2d  13844  rmodislmod  13847  lsssn0  13866  sraval  13933  qusrhm  14024  gsumfzfsumlemm  14075  expghmap  14095  mulgghm2  14096  mulgrhm  14097  zlmval  14115  znval  14124  psrval  14152  cnfval  14362  cnpfval  14363  ispsmet  14491  psmet0  14495  psmettri2  14496  psmetres2  14501  ismet  14512  isxmet  14513  xmettri2  14529  xmetres2  14547  xblss2  14573  xmstri2  14638  mstri2  14639  xmstri  14640  mstri  14641  xmstri3  14642  mstri3  14643  msrtri  14644  comet  14667  bdxmet  14669  txmetcnp  14686  metcnpd  14688  cnmet  14698  ioo2bl  14711  fsumcncntop  14724  elcncf  14728  mulc1cncf  14744  cncfco  14746  cncfcncntop  14748  cncfmptc  14750  cncfmptid  14751  addccncf  14754  cdivcncfap  14758  negcncf  14759  mulcncflem  14761  limccnp2cntop  14831  reldvg  14833  dvfvalap  14835  eldvap  14836  dvconst  14846  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvexp  14860  dvrecap  14862  dveflem  14872  dvef  14873  elplyd  14887  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  plyadd  14897  plymul  14898  sinperlem  14943  sinmpi  14950  cosmpi  14951  sinppi  14952  cosppi  14953  efimpi  14954  sinhalfpip  14955  sinhalfpim  14956  coshalfpip  14957  coshalfpim  14958  ptolemy  14959  tangtx  14973  logdivlti  15016  rpcxpadd  15040  rpmulcxp  15044  rplogbchbase  15082  rprelogbmul  15087  binom4  15111  wilthlem1  15112  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsval4a  15138  lgsneg  15140  lgsdilem  15143  lgsdirprm  15150  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  gausslemma2dlem4  15180  gausslemma2dlem6  15183  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem2  15202  2sqlem3  15204  2sqlem4  15205  2sqlem8  15210  cvgcmp2nlemabs  15522  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trilpo  15533  redcwlpo  15545  nconstwlpolemgt0  15554  nconstwlpo  15556  neapmkv  15558