Theorem oveq12d 5906

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

Syntax hints:   → wi 4   = wceq 1363  (class class class)co 5888

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236  df-ov 5891

This theorem is referenced by:  oveq123d  5909  ovmpodxf  6014  ovmpodf  6020  caovdig  6063  caovdir2d  6065  caovdirg  6066  caovdilemd  6080  caovlem2d  6081  offval  6104  ofvalg  6106  offval2  6112  ofco  6115  caofinvl  6119  offres  6150  nnmsucr  6503  nndir  6505  ecovdi  6660  ecovidi  6661  dfplpq2  7367  dfmpq2  7368  addcmpblnq  7380  mulpipqqs  7386  addassnqg  7395  distrnqg  7400  ltaddnq  7420  halfnqq  7423  enq0tr  7447  addcmpblnq0  7456  addnq0mo  7460  addnnnq0  7462  nqnq0a  7467  distrnq0  7472  addassnq0  7475  distnq0r  7476  nq02m  7478  ltexpri  7626  cauappcvgprlemm  7658  cauappcvgprlemloc  7665  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  cauappcvgprlem1  7672  cauappcvgprlem2  7673  cauappcvgprlemlim  7674  cauappcvgpr  7675  caucvgprlemnkj  7679  caucvgprlemnbj  7680  caucvgprlemm  7681  caucvgprlemloc  7688  caucvgprlemcl  7689  caucvgprlemladdfu  7690  caucvgprlemladdrl  7691  caucvgprlem2  7693  caucvgpr  7695  caucvgprprlemelu  7699  caucvgprprlemcbv  7700  caucvgprprlemval  7701  caucvgprprlemmu  7708  caucvgprprlemopu  7712  caucvgprprlemloc  7716  caucvgprprlemclphr  7718  caucvgprprlemexbt  7719  caucvgprprlem2  7723  mulcmpblnrlemg  7753  mulsrmo  7757  mulsrpr  7759  mulcomsrg  7770  distrsrg  7772  recexgt0sr  7786  mulgt0sr  7791  mulextsr1lem  7793  caucvgsrlemgt1  7808  caucvgsr  7815  addcnsr  7847  mulcnsr  7848  recidpirqlemcalc  7870  axaddcl  7877  axmulcl  7879  axmulcom  7884  axmulass  7886  axdistr  7887  axcaucvglemcau  7911  axcaucvglemres  7912  adddir  7962  muladd11  8104  1p1times  8105  muladd11r  8127  pnpcan2  8211  muladd  8355  subdir  8357  mulsub  8372  mulreim  8575  apadd1  8579  mulext1  8583  recextlem1  8622  muleqadd  8639  divdirap  8668  divadddivap  8698  conjmulap  8700  divcanap5rd  8789  subrecap  8810  xp1d2m1eqxm1d2  9185  div4p1lem1div2  9186  cnref1o  9664  xnegid  9873  xposdif  9896  xleaddadd  9901  icoshftf1o  10005  lincmb01cmp  10017  iccf1o  10018  fz01en  10067  fzrev3  10101  fzrevral2  10120  fzrevral3  10121  fzshftral  10122  fzoaddel2  10207  fzosubel  10208  fzosubel2  10209  fzocatel  10213  modqsubdir  10407  addmodlteq  10412  frecuzrdgsuc  10428  frecfzen2  10441  iseqovex  10470  seqvalcd  10473  seq3caopr3  10495  seq3f1olemqsumkj  10512  seq3f1olemqsumk  10513  seq3f1olemqsum  10514  seq3id3  10521  seqfeq3  10526  seq3distr  10527  ser3le  10532  mulexp  10573  mulexpzap  10574  expaddzap  10578  expubnd  10591  subsq  10641  binom2  10646  binom21  10647  binom2sub  10648  binom2sub1  10649  binom3  10652  sqoddm1div8  10688  mulsubdivbinom2ap  10705  nn0opthlem1d  10714  nn0opthd  10716  facp1  10724  facubnd  10739  bcval  10743  bcn1  10752  bcm1k  10754  bcp1n  10755  bcp1nk  10756  bcval5  10757  bcn2  10758  bcpasc  10760  hashun  10799  hashfz  10815  crre  10880  replim  10882  remullem  10894  remul2  10896  immul2  10903  cjcj  10906  cjadd  10907  ipcnval  10909  cjmulval  10911  cjneg  10913  imval2  10917  cjreim  10926  cvg1nlemcau  11007  cvg1nlemres  11008  resqrexlemp1rp  11029  resqrexlemfp1  11032  resqrexlemcalc1  11037  resqrexlemcalc2  11038  resqrex  11049  sqabsadd  11078  sqabssub  11079  absreimsq  11090  recan  11132  amgm2  11141  maxabslemab  11229  maxabslemval  11231  max0addsup  11242  minabs  11258  bdtrilem  11261  bdtri  11262  xrmaxadd  11283  xrminadd  11297  xrbdtri  11298  subcn2  11333  reccn2ap  11335  climle  11356  climcvg1nlem  11371  serf0  11374  fsumadd  11428  fsumsplit  11429  sumpr  11435  sumtp  11436  isumadd  11453  sumsplitdc  11454  fsum2dlemstep  11456  fsumshftm  11467  fisumrev2  11468  fsumconst  11476  modfsummodlemstep  11479  telfsumo  11488  fsumparts  11492  binomlem  11505  binom  11506  binom1dif  11509  bcxmaslem1  11510  isumsplit  11513  isumnn0nn  11515  arisum  11520  arisum2  11521  trireciplem  11522  trirecip  11523  geosergap  11528  geo2sum  11536  geo2sum2  11537  cvgratnnlemsumlt  11550  mertenslemi1  11557  mertensabs  11559  fprodmul  11613  fprodsplitdc  11618  fprodabs  11638  fprod2dlemstep  11644  fproddivapf  11653  eftabs  11678  eftvalcn  11679  efcllemp  11680  ege2le3  11693  efcj  11695  efaddlem  11696  efsep  11713  ef4p  11716  efgt1p2  11717  efgt1p  11718  sinval  11724  cosval  11725  tanvalap  11730  tanval2ap  11735  tanval3ap  11736  efi4p  11739  sinneg  11748  cosneg  11749  tannegap  11750  efival  11754  efmival  11755  sinadd  11758  cosadd  11759  tanaddaplem  11760  tanaddap  11761  sinsub  11762  cossub  11763  addsin  11764  subsin  11765  sinmul  11766  cosmul  11767  addcos  11768  subcos  11769  sincossq  11770  cos2t  11772  sin01bnd  11779  cos01bnd  11780  efieq1re  11793  demoivreALT  11795  dvds2ln  11845  odd2np1lem  11891  gcdaddm  11999  bezoutlemnewy  12011  dfgcd3  12025  dvdsgcd  12027  mulgcd  12031  mulgcdr  12033  gcddiv  12034  sqgcd  12044  lcmgcdlem  12091  lcmgcd  12092  qredeu  12111  divgcdcoprm0  12115  cncongr1  12117  oddpwdclemdc  12187  sqrt2irraplemnn  12193  qnumdenbi  12206  zgcdsq  12215  hashdvds  12235  phiprmpw  12236  phimullem  12239  eulerthlema  12244  prmdiv  12249  modprm0  12268  coprimeprodsq  12271  pythagtriplem1  12279  pythagtriplem12  12289  pythagtriplem14  12291  pythagtriplem15  12292  pythagtriplem16  12293  pythagtriplem17  12294  pythagtriplem19  12296  pcval  12310  pcmul  12315  pcdiv  12316  pcqmul  12317  pcid  12337  pcaddlem  12352  pcmpt  12355  pcmpt2  12356  pcmptdvds  12357  pcbc  12363  4sqlem4  12404  mul4sqlem  12405  mul4sq  12406  ennnfonelemp1  12421  nninfdclemp1  12465  ressvalsets  12538  topnvalg  12718  topnpropgd  12720  prdsex  12736  qusval  12762  qusex  12764  qusaddvallemg  12771  xpsval  12790  ismhm  12875  mhmf1o  12883  0mhm  12899  mhmco  12903  mhmeql  12905  isgrpid2  12945  grpnpcan  12997  imasgrp2  13013  mhmmnd  13019  mulgnndir  13052  mulgdir  13055  isnsg3  13107  isghm  13138  ghmnsgima  13162  ghmf1o  13169  conjghm  13170  qusghm  13176  ablsub4  13207  ghmcmn  13220  mgpvalg  13232  mgptopng  13238  mgpress  13240  rngdi  13249  rngdir  13250  rngpropd  13264  imasrng  13265  srglmhm  13302  srgrmhm  13303  ringo2times  13337  ringcom  13340  ringpropd  13347  ring1  13366  imasring  13369  opprvalg  13374  opprrng  13382  opprring  13384  invrfvald  13427  dvrvald  13439  dvrdir  13448  rdivmuldivd  13449  islmod  13537  lmodlema  13538  islmodd  13539  lmodcom  13579  lmodnegadd  13582  lmodprop2d  13594  rmodislmod  13597  lsssn0  13616  sraval  13683  zlmval  13842  cnfval  14047  cnpfval  14048  ispsmet  14176  psmet0  14180  psmettri2  14181  psmetres2  14186  ismet  14197  isxmet  14198  xmettri2  14214  xmetres2  14232  xblss2  14258  xmstri2  14323  mstri2  14324  xmstri  14325  mstri  14326  xmstri3  14327  mstri3  14328  msrtri  14329  comet  14352  bdxmet  14354  txmetcnp  14371  metcnpd  14373  cnmet  14383  ioo2bl  14396  fsumcncntop  14409  elcncf  14413  mulc1cncf  14429  cncfco  14431  cncfcncntop  14433  cncfmptc  14435  cncfmptid  14436  addccncf  14439  cdivcncfap  14440  negcncf  14441  mulcncflem  14443  limccnp2cntop  14499  reldvg  14501  dvfvalap  14503  eldvap  14504  dvconst  14514  dvaddxxbr  14518  dvmulxxbr  14519  dvcoapbr  14524  dvcjbr  14525  dvexp  14528  dvrecap  14530  dveflem  14540  dvef  14541  sinperlem  14582  sinmpi  14589  cosmpi  14590  sinppi  14591  cosppi  14592  efimpi  14593  sinhalfpip  14594  sinhalfpim  14595  coshalfpip  14596  coshalfpim  14597  ptolemy  14598  tangtx  14612  logdivlti  14655  rpcxpadd  14679  rpmulcxp  14683  rplogbchbase  14721  rprelogbmul  14726  binom4  14750  lgsval  14758  lgsfvalg  14759  lgsval2lem  14764  lgsval4a  14776  lgsneg  14778  lgsdilem  14781  lgsdirprm  14788  lgsdir  14789  lgsdilem2  14790  lgsdi  14791  lgsne0  14792  lgseisenlem2  14804  2sqlem2  14815  2sqlem3  14817  2sqlem4  14818  2sqlem8  14823  cvgcmp2nlemabs  15134  trilpolemclim  15138  trilpolemcl  15139  trilpolemisumle  15140  trilpolemeq1  15142  trilpolemlt1  15143  trilpo  15145  redcwlpo  15157  nconstwlpolemgt0  15166  nconstwlpo  15168  neapmkv  15170