Theorem oveq12d 5868

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

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

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 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853

This theorem is referenced by:  oveq123d  5871  ovmpodxf  5975  ovmpodf  5981  caovdig  6024  caovdir2d  6026  caovdirg  6027  caovdilemd  6041  caovlem2d  6042  offval  6065  ofvalg  6067  offval2  6073  ofco  6076  caofinvl  6080  offres  6111  nnmsucr  6464  nndir  6466  ecovdi  6620  ecovidi  6621  dfplpq2  7303  dfmpq2  7304  addcmpblnq  7316  mulpipqqs  7322  addassnqg  7331  distrnqg  7336  ltaddnq  7356  halfnqq  7359  enq0tr  7383  addcmpblnq0  7392  addnq0mo  7396  addnnnq0  7398  nqnq0a  7403  distrnq0  7408  addassnq0  7411  distnq0r  7412  nq02m  7414  ltexpri  7562  cauappcvgprlemm  7594  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  cauappcvgprlem2  7609  cauappcvgprlemlim  7610  cauappcvgpr  7611  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem2  7629  caucvgpr  7631  caucvgprprlemelu  7635  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemmu  7644  caucvgprprlemopu  7648  caucvgprprlemloc  7652  caucvgprprlemclphr  7654  caucvgprprlemexbt  7655  caucvgprprlem2  7659  mulcmpblnrlemg  7689  mulsrmo  7693  mulsrpr  7695  mulcomsrg  7706  distrsrg  7708  recexgt0sr  7722  mulgt0sr  7727  mulextsr1lem  7729  caucvgsrlemgt1  7744  caucvgsr  7751  addcnsr  7783  mulcnsr  7784  recidpirqlemcalc  7806  axaddcl  7813  axmulcl  7815  axmulcom  7820  axmulass  7822  axdistr  7823  axcaucvglemcau  7847  axcaucvglemres  7848  adddir  7898  muladd11  8039  1p1times  8040  muladd11r  8062  pnpcan2  8146  muladd  8290  subdir  8292  mulsub  8307  mulreim  8510  apadd1  8514  mulext1  8518  recextlem1  8556  muleqadd  8573  divdirap  8601  divadddivap  8631  conjmulap  8633  divcanap5rd  8722  subrecap  8743  xp1d2m1eqxm1d2  9117  div4p1lem1div2  9118  cnref1o  9596  xnegid  9803  xposdif  9826  xleaddadd  9831  icoshftf1o  9935  lincmb01cmp  9947  iccf1o  9948  fz01en  9996  fzrev3  10030  fzrevral2  10049  fzrevral3  10050  fzshftral  10051  fzoaddel2  10136  fzosubel  10137  fzosubel2  10138  fzocatel  10142  modqsubdir  10336  addmodlteq  10341  frecuzrdgsuc  10357  frecfzen2  10370  iseqovex  10399  seqvalcd  10402  seq3caopr3  10424  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  seq3id3  10450  seqfeq3  10455  seq3distr  10456  ser3le  10461  mulexp  10502  mulexpzap  10503  expaddzap  10507  expubnd  10520  subsq  10569  binom2  10574  binom21  10575  binom2sub  10576  binom2sub1  10577  binom3  10580  sqoddm1div8  10616  nn0opthlem1d  10641  nn0opthd  10643  facp1  10651  facubnd  10666  bcval  10670  bcn1  10679  bcm1k  10681  bcp1n  10682  bcp1nk  10683  bcval5  10684  bcn2  10685  bcpasc  10687  hashun  10727  hashfz  10743  crre  10808  replim  10810  remullem  10822  remul2  10824  immul2  10831  cjcj  10834  cjadd  10835  ipcnval  10837  cjmulval  10839  cjneg  10841  imval2  10845  cjreim  10854  cvg1nlemcau  10935  cvg1nlemres  10936  resqrexlemp1rp  10957  resqrexlemfp1  10960  resqrexlemcalc1  10965  resqrexlemcalc2  10966  resqrex  10977  sqabsadd  11006  sqabssub  11007  absreimsq  11018  recan  11060  amgm2  11069  maxabslemab  11157  maxabslemval  11159  max0addsup  11170  minabs  11186  bdtrilem  11189  bdtri  11190  xrmaxadd  11211  xrminadd  11225  xrbdtri  11226  subcn2  11261  reccn2ap  11263  climle  11284  climcvg1nlem  11299  serf0  11302  fsumadd  11356  fsumsplit  11357  sumpr  11363  sumtp  11364  isumadd  11381  sumsplitdc  11382  fsum2dlemstep  11384  fsumshftm  11395  fisumrev2  11396  fsumconst  11404  modfsummodlemstep  11407  telfsumo  11416  fsumparts  11420  binomlem  11433  binom  11434  binom1dif  11437  bcxmaslem1  11438  isumsplit  11441  isumnn0nn  11443  arisum  11448  arisum2  11449  trireciplem  11450  trirecip  11451  geosergap  11456  geo2sum  11464  geo2sum2  11465  cvgratnnlemsumlt  11478  mertenslemi1  11485  mertensabs  11487  fprodmul  11541  fprodsplitdc  11546  fprodabs  11566  fprod2dlemstep  11572  fproddivapf  11581  eftabs  11606  eftvalcn  11607  efcllemp  11608  ege2le3  11621  efcj  11623  efaddlem  11624  efsep  11641  ef4p  11644  efgt1p2  11645  efgt1p  11646  sinval  11652  cosval  11653  tanvalap  11658  tanval2ap  11663  tanval3ap  11664  efi4p  11667  sinneg  11676  cosneg  11677  tannegap  11678  efival  11682  efmival  11683  sinadd  11686  cosadd  11687  tanaddaplem  11688  tanaddap  11689  sinsub  11690  cossub  11691  addsin  11692  subsin  11693  sinmul  11694  cosmul  11695  addcos  11696  subcos  11697  sincossq  11698  cos2t  11700  sin01bnd  11707  cos01bnd  11708  efieq1re  11721  demoivreALT  11723  dvds2ln  11773  odd2np1lem  11818  gcdaddm  11926  bezoutlemnewy  11938  dfgcd3  11952  dvdsgcd  11954  mulgcd  11958  mulgcdr  11960  gcddiv  11961  sqgcd  11971  lcmgcdlem  12018  lcmgcd  12019  qredeu  12038  divgcdcoprm0  12042  cncongr1  12044  oddpwdclemdc  12114  sqrt2irraplemnn  12120  qnumdenbi  12133  zgcdsq  12142  hashdvds  12162  phiprmpw  12163  phimullem  12166  eulerthlema  12171  prmdiv  12176  modprm0  12195  coprimeprodsq  12198  pythagtriplem1  12206  pythagtriplem12  12216  pythagtriplem14  12218  pythagtriplem15  12219  pythagtriplem16  12220  pythagtriplem17  12221  pythagtriplem19  12223  pcval  12237  pcmul  12242  pcdiv  12243  pcqmul  12244  pcid  12264  pcaddlem  12279  pcmpt  12282  pcmpt2  12283  pcmptdvds  12284  pcbc  12290  4sqlem4  12331  mul4sqlem  12332  mul4sq  12333  ennnfonelemp1  12348  nninfdclemp1  12392  ressid2  12463  ressval2  12464  topnvalg  12577  topnpropgd  12579  ismhm  12671  mhmf1o  12679  0mhm  12690  mhmco  12691  mhmeql  12693  cnfval  12909  cnpfval  12910  ispsmet  13038  psmet0  13042  psmettri2  13043  psmetres2  13048  ismet  13059  isxmet  13060  xmettri2  13076  xmetres2  13094  xblss2  13120  xmstri2  13185  mstri2  13186  xmstri  13187  mstri  13188  xmstri3  13189  mstri3  13190  msrtri  13191  comet  13214  bdxmet  13216  txmetcnp  13233  metcnpd  13235  cnmet  13245  ioo2bl  13258  fsumcncntop  13271  elcncf  13275  mulc1cncf  13291  cncfco  13293  cncfcncntop  13295  cncfmptc  13297  cncfmptid  13298  addccncf  13301  cdivcncfap  13302  negcncf  13303  mulcncflem  13305  limccnp2cntop  13361  reldvg  13363  dvfvalap  13365  eldvap  13366  dvconst  13376  dvaddxxbr  13380  dvmulxxbr  13381  dvcoapbr  13386  dvcjbr  13387  dvexp  13390  dvrecap  13392  dveflem  13402  dvef  13403  sinperlem  13444  sinmpi  13451  cosmpi  13452  sinppi  13453  cosppi  13454  efimpi  13455  sinhalfpip  13456  sinhalfpim  13457  coshalfpip  13458  coshalfpim  13459  ptolemy  13460  tangtx  13474  logdivlti  13517  rpcxpadd  13541  rpmulcxp  13545  rplogbchbase  13583  rprelogbmul  13588  binom4  13612  lgsval  13620  lgsfvalg  13621  lgsval2lem  13626  lgsval4a  13638  lgsneg  13640  lgsdilem  13643  lgsdirprm  13650  lgsdir  13651  lgsdilem2  13652  lgsdi  13653  lgsne0  13654  2sqlem2  13666  2sqlem3  13668  2sqlem4  13669  2sqlem8  13674  cvgcmp2nlemabs  13986  trilpolemclim  13990  trilpolemcl  13991  trilpolemisumle  13992  trilpolemeq1  13994  trilpolemlt1  13995  trilpo  13997  redcwlpo  14009  nconstwlpolemgt0  14017  nconstwlpo  14019  neapmkv  14021