Theorem oveq12d 5871

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

Syntax hints:   → wi 4   = wceq 1348  (class class class)co 5853

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  oveq123d  5874  ovmpodxf  5978  ovmpodf  5984  caovdig  6027  caovdir2d  6029  caovdirg  6030  caovdilemd  6044  caovlem2d  6045  offval  6068  ofvalg  6070  offval2  6076  ofco  6079  caofinvl  6083  offres  6114  nnmsucr  6467  nndir  6469  ecovdi  6624  ecovidi  6625  dfplpq2  7316  dfmpq2  7317  addcmpblnq  7329  mulpipqqs  7335  addassnqg  7344  distrnqg  7349  ltaddnq  7369  halfnqq  7372  enq0tr  7396  addcmpblnq0  7405  addnq0mo  7409  addnnnq0  7411  nqnq0a  7416  distrnq0  7421  addassnq0  7424  distnq0r  7425  nq02m  7427  ltexpri  7575  cauappcvgprlemm  7607  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemmu  7657  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem2  7672  mulcmpblnrlemg  7702  mulsrmo  7706  mulsrpr  7708  mulcomsrg  7719  distrsrg  7721  recexgt0sr  7735  mulgt0sr  7740  mulextsr1lem  7742  caucvgsrlemgt1  7757  caucvgsr  7764  addcnsr  7796  mulcnsr  7797  recidpirqlemcalc  7819  axaddcl  7826  axmulcl  7828  axmulcom  7833  axmulass  7835  axdistr  7836  axcaucvglemcau  7860  axcaucvglemres  7861  adddir  7911  muladd11  8052  1p1times  8053  muladd11r  8075  pnpcan2  8159  muladd  8303  subdir  8305  mulsub  8320  mulreim  8523  apadd1  8527  mulext1  8531  recextlem1  8569  muleqadd  8586  divdirap  8614  divadddivap  8644  conjmulap  8646  divcanap5rd  8735  subrecap  8756  xp1d2m1eqxm1d2  9130  div4p1lem1div2  9131  cnref1o  9609  xnegid  9816  xposdif  9839  xleaddadd  9844  icoshftf1o  9948  lincmb01cmp  9960  iccf1o  9961  fz01en  10009  fzrev3  10043  fzrevral2  10062  fzrevral3  10063  fzshftral  10064  fzoaddel2  10149  fzosubel  10150  fzosubel2  10151  fzocatel  10155  modqsubdir  10349  addmodlteq  10354  frecuzrdgsuc  10370  frecfzen2  10383  iseqovex  10412  seqvalcd  10415  seq3caopr3  10437  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3id3  10463  seqfeq3  10468  seq3distr  10469  ser3le  10474  mulexp  10515  mulexpzap  10516  expaddzap  10520  expubnd  10533  subsq  10582  binom2  10587  binom21  10588  binom2sub  10589  binom2sub1  10590  binom3  10593  sqoddm1div8  10629  nn0opthlem1d  10654  nn0opthd  10656  facp1  10664  facubnd  10679  bcval  10683  bcn1  10692  bcm1k  10694  bcp1n  10695  bcp1nk  10696  bcval5  10697  bcn2  10698  bcpasc  10700  hashun  10740  hashfz  10756  crre  10821  replim  10823  remullem  10835  remul2  10837  immul2  10844  cjcj  10847  cjadd  10848  ipcnval  10850  cjmulval  10852  cjneg  10854  imval2  10858  cjreim  10867  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrex  10990  sqabsadd  11019  sqabssub  11020  absreimsq  11031  recan  11073  amgm2  11082  maxabslemab  11170  maxabslemval  11172  max0addsup  11183  minabs  11199  bdtrilem  11202  bdtri  11203  xrmaxadd  11224  xrminadd  11238  xrbdtri  11239  subcn2  11274  reccn2ap  11276  climle  11297  climcvg1nlem  11312  serf0  11315  fsumadd  11369  fsumsplit  11370  sumpr  11376  sumtp  11377  isumadd  11394  sumsplitdc  11395  fsum2dlemstep  11397  fsumshftm  11408  fisumrev2  11409  fsumconst  11417  modfsummodlemstep  11420  telfsumo  11429  fsumparts  11433  binomlem  11446  binom  11447  binom1dif  11450  bcxmaslem1  11451  isumsplit  11454  isumnn0nn  11456  arisum  11461  arisum2  11462  trireciplem  11463  trirecip  11464  geosergap  11469  geo2sum  11477  geo2sum2  11478  cvgratnnlemsumlt  11491  mertenslemi1  11498  mertensabs  11500  fprodmul  11554  fprodsplitdc  11559  fprodabs  11579  fprod2dlemstep  11585  fproddivapf  11594  eftabs  11619  eftvalcn  11620  efcllemp  11621  ege2le3  11634  efcj  11636  efaddlem  11637  efsep  11654  ef4p  11657  efgt1p2  11658  efgt1p  11659  sinval  11665  cosval  11666  tanvalap  11671  tanval2ap  11676  tanval3ap  11677  efi4p  11680  sinneg  11689  cosneg  11690  tannegap  11691  efival  11695  efmival  11696  sinadd  11699  cosadd  11700  tanaddaplem  11701  tanaddap  11702  sinsub  11703  cossub  11704  addsin  11705  subsin  11706  sinmul  11707  cosmul  11708  addcos  11709  subcos  11710  sincossq  11711  cos2t  11713  sin01bnd  11720  cos01bnd  11721  efieq1re  11734  demoivreALT  11736  dvds2ln  11786  odd2np1lem  11831  gcdaddm  11939  bezoutlemnewy  11951  dfgcd3  11965  dvdsgcd  11967  mulgcd  11971  mulgcdr  11973  gcddiv  11974  sqgcd  11984  lcmgcdlem  12031  lcmgcd  12032  qredeu  12051  divgcdcoprm0  12055  cncongr1  12057  oddpwdclemdc  12127  sqrt2irraplemnn  12133  qnumdenbi  12146  zgcdsq  12155  hashdvds  12175  phiprmpw  12176  phimullem  12179  eulerthlema  12184  prmdiv  12189  modprm0  12208  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  pythagtriplem19  12236  pcval  12250  pcmul  12255  pcdiv  12256  pcqmul  12257  pcid  12277  pcaddlem  12292  pcmpt  12295  pcmpt2  12296  pcmptdvds  12297  pcbc  12303  4sqlem4  12344  mul4sqlem  12345  mul4sq  12346  ennnfonelemp1  12361  nninfdclemp1  12405  ressid2  12477  ressval2  12478  topnvalg  12591  topnpropgd  12593  ismhm  12685  mhmf1o  12693  0mhm  12704  mhmco  12705  mhmeql  12707  isgrpid2  12743  cnfval  12988  cnpfval  12989  ispsmet  13117  psmet0  13121  psmettri2  13122  psmetres2  13127  ismet  13138  isxmet  13139  xmettri2  13155  xmetres2  13173  xblss2  13199  xmstri2  13264  mstri2  13265  xmstri  13266  mstri  13267  xmstri3  13268  mstri3  13269  msrtri  13270  comet  13293  bdxmet  13295  txmetcnp  13312  metcnpd  13314  cnmet  13324  ioo2bl  13337  fsumcncntop  13350  elcncf  13354  mulc1cncf  13370  cncfco  13372  cncfcncntop  13374  cncfmptc  13376  cncfmptid  13377  addccncf  13380  cdivcncfap  13381  negcncf  13382  mulcncflem  13384  limccnp2cntop  13440  reldvg  13442  dvfvalap  13444  eldvap  13445  dvconst  13455  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvexp  13469  dvrecap  13471  dveflem  13481  dvef  13482  sinperlem  13523  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  efimpi  13534  sinhalfpip  13535  sinhalfpim  13536  coshalfpip  13537  coshalfpim  13538  ptolemy  13539  tangtx  13553  logdivlti  13596  rpcxpadd  13620  rpmulcxp  13624  rplogbchbase  13662  rprelogbmul  13667  binom4  13691  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsval4a  13717  lgsneg  13719  lgsdilem  13722  lgsdirprm  13729  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  2sqlem2  13745  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  cvgcmp2nlemabs  14064  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trilpo  14075  redcwlpo  14087  nconstwlpolemgt0  14095  nconstwlpo  14097  neapmkv  14099