Theorem oveq12d 5724

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

Syntax hints:   → wi 4   = wceq 1299  (class class class)co 5706

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067  df-ov 5709

This theorem is referenced by:  oveq123d  5727  ovmpodxf  5828  ovmpodf  5834  caovdig  5877  caovdir2d  5879  caovdirg  5880  caovdilemd  5894  caovlem2d  5895  offval  5921  fnofval  5923  offval2  5928  ofco  5931  caofinvl  5935  offres  5964  nnmsucr  6314  nndir  6316  ecovdi  6470  ecovidi  6471  dfplpq2  7063  dfmpq2  7064  addcmpblnq  7076  mulpipqqs  7082  addassnqg  7091  distrnqg  7096  ltaddnq  7116  halfnqq  7119  enq0tr  7143  addcmpblnq0  7152  addnq0mo  7156  addnnnq0  7158  nqnq0a  7163  distrnq0  7168  addassnq0  7171  distnq0r  7172  nq02m  7174  ltexpri  7322  cauappcvgprlemm  7354  cauappcvgprlemloc  7361  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlem2  7369  cauappcvgprlemlim  7370  cauappcvgpr  7371  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem2  7389  caucvgpr  7391  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemmu  7404  caucvgprprlemopu  7408  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  caucvgprprlem2  7419  mulcmpblnrlemg  7436  mulsrmo  7440  mulsrpr  7442  mulcomsrg  7453  distrsrg  7455  recexgt0sr  7469  mulgt0sr  7473  mulextsr1lem  7475  caucvgsrlemgt1  7490  caucvgsr  7497  addcnsr  7521  mulcnsr  7522  recidpirqlemcalc  7544  axaddcl  7551  axmulcl  7553  axmulcom  7556  axmulass  7558  axdistr  7559  axcaucvglemcau  7583  axcaucvglemres  7584  adddir  7629  muladd11  7766  1p1times  7767  muladd11r  7789  pnpcan2  7873  muladd  8013  subdir  8015  mulsub  8030  mulreim  8232  apadd1  8236  mulext1  8240  recextlem1  8273  muleqadd  8290  divdirap  8318  divadddivap  8348  conjmulap  8350  divcanap5rd  8439  xp1d2m1eqxm1d2  8824  div4p1lem1div2  8825  cnref1o  9290  xnegid  9483  xposdif  9506  xleaddadd  9511  icoshftf1o  9615  lincmb01cmp  9627  iccf1o  9628  fz01en  9674  fzrev3  9708  fzrevral2  9727  fzrevral3  9728  fzshftral  9729  fzoaddel2  9811  fzosubel  9812  fzosubel2  9813  fzocatel  9817  modqsubdir  10007  addmodlteq  10012  frecuzrdgsuc  10028  frecfzen2  10041  iseqovex  10070  seqvalcd  10073  seq3caopr3  10095  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3id3  10121  seqfeq3  10126  seq3distr  10127  ser3le  10132  mulexp  10173  mulexpzap  10174  expaddzap  10178  expubnd  10191  subsq  10240  binom2  10244  binom21  10245  binom2sub  10246  binom2sub1  10247  binom3  10250  sqoddm1div8  10285  nn0opthlem1d  10307  nn0opthd  10309  facp1  10317  facubnd  10332  bcval  10336  bcn1  10345  bcm1k  10347  bcp1n  10348  bcp1nk  10349  bcval5  10350  bcn2  10351  bcpasc  10353  hashun  10392  hashfz  10408  crre  10470  replim  10472  remullem  10484  remul2  10486  immul2  10493  cjcj  10496  cjadd  10497  ipcnval  10499  cjmulval  10501  cjneg  10503  imval2  10507  cjreim  10516  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemp1rp  10618  resqrexlemfp1  10621  resqrexlemcalc1  10626  resqrexlemcalc2  10627  resqrex  10638  sqabsadd  10667  sqabssub  10668  absreimsq  10679  recan  10721  amgm2  10730  maxabslemab  10818  maxabslemval  10820  max0addsup  10831  minabs  10846  bdtrilem  10849  bdtri  10850  xrmaxadd  10869  xrminadd  10883  xrbdtri  10884  subcn2  10919  reccn2ap  10921  climle  10942  climcvg1nlem  10957  serf0  10960  fsumadd  11014  fsumsplit  11015  sumpr  11021  sumtp  11022  isumadd  11039  sumsplitdc  11040  fsum2dlemstep  11042  fsumshftm  11053  fisumrev2  11054  fsumconst  11062  modfsummodlemstep  11065  telfsumo  11074  fsumparts  11078  binomlem  11091  binom  11092  binom1dif  11095  bcxmaslem1  11096  isumsplit  11099  isumnn0nn  11101  arisum  11106  arisum2  11107  trireciplem  11108  trirecip  11109  geosergap  11114  geo2sum  11122  geo2sum2  11123  cvgratnnlemsumlt  11136  mertenslemi1  11143  mertensabs  11145  eftabs  11160  eftvalcn  11161  efcllemp  11162  ege2le3  11175  efcj  11177  efaddlem  11178  efsep  11195  ef4p  11198  efgt1p2  11199  efgt1p  11200  sinval  11207  cosval  11208  tanvalap  11213  tanval2ap  11218  tanval3ap  11219  efi4p  11222  sinneg  11231  cosneg  11232  tannegap  11233  efival  11237  efmival  11238  sinadd  11241  cosadd  11242  tanaddaplem  11243  tanaddap  11244  sinsub  11245  cossub  11246  addsin  11247  subsin  11248  sinmul  11249  cosmul  11250  addcos  11251  subcos  11252  sincossq  11253  cos2t  11255  sin01bnd  11262  cos01bnd  11263  efieq1re  11275  demoivreALT  11277  dvds2ln  11321  odd2np1lem  11364  gcdaddm  11467  bezoutlemnewy  11477  dfgcd3  11491  dvdsgcd  11493  mulgcd  11497  mulgcdr  11499  gcddiv  11500  sqgcd  11510  lcmgcdlem  11551  lcmgcd  11552  qredeu  11571  divgcdcoprm0  11575  cncongr1  11577  oddpwdclemdc  11643  sqrt2irraplemnn  11649  qnumdenbi  11662  zgcdsq  11671  hashdvds  11689  phiprmpw  11690  phimullem  11693  ennnfonelemp1  11711  ressid2  11800  ressval2  11801  topnvalg  11914  topnpropgd  11916  cnfval  12145  cnpfval  12146  ispsmet  12251  psmet0  12255  psmettri2  12256  psmetres2  12261  ismet  12272  isxmet  12273  xmettri2  12289  xmetres2  12307  xblss2  12333  xmstri2  12398  mstri2  12399  xmstri  12400  mstri  12401  xmstri3  12402  mstri3  12403  msrtri  12404  comet  12427  bdxmet  12429  metcnpd  12442  cnmet  12452  ioo2bl  12462  elcncf  12473  mulc1cncf  12489  cncfco  12491  cncfcncntop  12493  cncfmptc  12495  cncfmptid  12496  addccncf  12498  cdivcncfap  12499  negcncf  12500  mulcncflem  12502  reldvg  12521  dvfvalap  12523  eldvap  12524  dvconst  12534  cvgcmp2nlemabs  12811  trilpolemclim  12813  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818  trilpo  12820