Theorem oveq12d 5892

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

Syntax hints:   → wi 4   = wceq 1353  (class class class)co 5874

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  oveq123d  5895  ovmpodxf  5999  ovmpodf  6005  caovdig  6048  caovdir2d  6050  caovdirg  6051  caovdilemd  6065  caovlem2d  6066  offval  6089  ofvalg  6091  offval2  6097  ofco  6100  caofinvl  6104  offres  6135  nnmsucr  6488  nndir  6490  ecovdi  6645  ecovidi  6646  dfplpq2  7352  dfmpq2  7353  addcmpblnq  7365  mulpipqqs  7371  addassnqg  7380  distrnqg  7385  ltaddnq  7405  halfnqq  7408  enq0tr  7432  addcmpblnq0  7441  addnq0mo  7445  addnnnq0  7447  nqnq0a  7452  distrnq0  7457  addassnq0  7460  distnq0r  7461  nq02m  7463  ltexpri  7611  cauappcvgprlemm  7643  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlem2  7658  cauappcvgprlemlim  7659  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemmu  7693  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem2  7708  mulcmpblnrlemg  7738  mulsrmo  7742  mulsrpr  7744  mulcomsrg  7755  distrsrg  7757  recexgt0sr  7771  mulgt0sr  7776  mulextsr1lem  7778  caucvgsrlemgt1  7793  caucvgsr  7800  addcnsr  7832  mulcnsr  7833  recidpirqlemcalc  7855  axaddcl  7862  axmulcl  7864  axmulcom  7869  axmulass  7871  axdistr  7872  axcaucvglemcau  7896  axcaucvglemres  7897  adddir  7947  muladd11  8089  1p1times  8090  muladd11r  8112  pnpcan2  8196  muladd  8340  subdir  8342  mulsub  8357  mulreim  8560  apadd1  8564  mulext1  8568  recextlem1  8607  muleqadd  8624  divdirap  8653  divadddivap  8683  conjmulap  8685  divcanap5rd  8774  subrecap  8795  xp1d2m1eqxm1d2  9170  div4p1lem1div2  9171  cnref1o  9649  xnegid  9858  xposdif  9881  xleaddadd  9886  icoshftf1o  9990  lincmb01cmp  10002  iccf1o  10003  fz01en  10052  fzrev3  10086  fzrevral2  10105  fzrevral3  10106  fzshftral  10107  fzoaddel2  10192  fzosubel  10193  fzosubel2  10194  fzocatel  10198  modqsubdir  10392  addmodlteq  10397  frecuzrdgsuc  10413  frecfzen2  10426  iseqovex  10455  seqvalcd  10458  seq3caopr3  10480  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3id3  10506  seqfeq3  10511  seq3distr  10512  ser3le  10517  mulexp  10558  mulexpzap  10559  expaddzap  10563  expubnd  10576  subsq  10626  binom2  10631  binom21  10632  binom2sub  10633  binom2sub1  10634  binom3  10637  sqoddm1div8  10673  mulsubdivbinom2ap  10690  nn0opthlem1d  10699  nn0opthd  10701  facp1  10709  facubnd  10724  bcval  10728  bcn1  10737  bcm1k  10739  bcp1n  10740  bcp1nk  10741  bcval5  10742  bcn2  10743  bcpasc  10745  hashun  10784  hashfz  10800  crre  10865  replim  10867  remullem  10879  remul2  10881  immul2  10888  cjcj  10891  cjadd  10892  ipcnval  10894  cjmulval  10896  cjneg  10898  imval2  10902  cjreim  10911  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemp1rp  11014  resqrexlemfp1  11017  resqrexlemcalc1  11022  resqrexlemcalc2  11023  resqrex  11034  sqabsadd  11063  sqabssub  11064  absreimsq  11075  recan  11117  amgm2  11126  maxabslemab  11214  maxabslemval  11216  max0addsup  11227  minabs  11243  bdtrilem  11246  bdtri  11247  xrmaxadd  11268  xrminadd  11282  xrbdtri  11283  subcn2  11318  reccn2ap  11320  climle  11341  climcvg1nlem  11356  serf0  11359  fsumadd  11413  fsumsplit  11414  sumpr  11420  sumtp  11421  isumadd  11438  sumsplitdc  11439  fsum2dlemstep  11441  fsumshftm  11452  fisumrev2  11453  fsumconst  11461  modfsummodlemstep  11464  telfsumo  11473  fsumparts  11477  binomlem  11490  binom  11491  binom1dif  11494  bcxmaslem1  11495  isumsplit  11498  isumnn0nn  11500  arisum  11505  arisum2  11506  trireciplem  11507  trirecip  11508  geosergap  11513  geo2sum  11521  geo2sum2  11522  cvgratnnlemsumlt  11535  mertenslemi1  11542  mertensabs  11544  fprodmul  11598  fprodsplitdc  11603  fprodabs  11623  fprod2dlemstep  11629  fproddivapf  11638  eftabs  11663  eftvalcn  11664  efcllemp  11665  ege2le3  11678  efcj  11680  efaddlem  11681  efsep  11698  ef4p  11701  efgt1p2  11702  efgt1p  11703  sinval  11709  cosval  11710  tanvalap  11715  tanval2ap  11720  tanval3ap  11721  efi4p  11724  sinneg  11733  cosneg  11734  tannegap  11735  efival  11739  efmival  11740  sinadd  11743  cosadd  11744  tanaddaplem  11745  tanaddap  11746  sinsub  11747  cossub  11748  addsin  11749  subsin  11750  sinmul  11751  cosmul  11752  addcos  11753  subcos  11754  sincossq  11755  cos2t  11757  sin01bnd  11764  cos01bnd  11765  efieq1re  11778  demoivreALT  11780  dvds2ln  11830  odd2np1lem  11876  gcdaddm  11984  bezoutlemnewy  11996  dfgcd3  12010  dvdsgcd  12012  mulgcd  12016  mulgcdr  12018  gcddiv  12019  sqgcd  12029  lcmgcdlem  12076  lcmgcd  12077  qredeu  12096  divgcdcoprm0  12100  cncongr1  12102  oddpwdclemdc  12172  sqrt2irraplemnn  12178  qnumdenbi  12191  zgcdsq  12200  hashdvds  12220  phiprmpw  12221  phimullem  12224  eulerthlema  12229  prmdiv  12234  modprm0  12253  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  pythagtriplem19  12281  pcval  12295  pcmul  12300  pcdiv  12301  pcqmul  12302  pcid  12322  pcaddlem  12337  pcmpt  12340  pcmpt2  12341  pcmptdvds  12342  pcbc  12348  4sqlem4  12389  mul4sqlem  12390  mul4sq  12391  ennnfonelemp1  12406  nninfdclemp1  12450  ressvalsets  12523  topnvalg  12699  topnpropgd  12701  prdsex  12717  qusval  12743  qusaddvallemg  12751  xpsval  12770  ismhm  12852  mhmf1o  12860  0mhm  12872  mhmco  12873  mhmeql  12875  isgrpid2  12912  grpnpcan  12961  mhmmnd  12979  mulgnndir  13010  mulgdir  13013  isnsg3  13065  ablsub4  13114  mgpvalg  13131  mgptopng  13137  mgpress  13139  srglmhm  13174  srgrmhm  13175  rngo2times  13209  ringcom  13212  ringpropd  13215  ring1  13234  opprvalg  13239  opprring  13247  invrfvald  13289  dvrvald  13301  dvrdir  13310  rdivmuldivd  13311  islmod  13379  lmodlema  13380  islmodd  13381  cnfval  13664  cnpfval  13665  ispsmet  13793  psmet0  13797  psmettri2  13798  psmetres2  13803  ismet  13814  isxmet  13815  xmettri2  13831  xmetres2  13849  xblss2  13875  xmstri2  13940  mstri2  13941  xmstri  13942  mstri  13943  xmstri3  13944  mstri3  13945  msrtri  13946  comet  13969  bdxmet  13971  txmetcnp  13988  metcnpd  13990  cnmet  14000  ioo2bl  14013  fsumcncntop  14026  elcncf  14030  mulc1cncf  14046  cncfco  14048  cncfcncntop  14050  cncfmptc  14052  cncfmptid  14053  addccncf  14056  cdivcncfap  14057  negcncf  14058  mulcncflem  14060  limccnp2cntop  14116  reldvg  14118  dvfvalap  14120  eldvap  14121  dvconst  14131  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvexp  14145  dvrecap  14147  dveflem  14157  dvef  14158  sinperlem  14199  sinmpi  14206  cosmpi  14207  sinppi  14208  cosppi  14209  efimpi  14210  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  ptolemy  14215  tangtx  14229  logdivlti  14272  rpcxpadd  14296  rpmulcxp  14300  rplogbchbase  14338  rprelogbmul  14343  binom4  14367  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsval4a  14393  lgsneg  14395  lgsdilem  14398  lgsdirprm  14405  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgseisenlem2  14421  2sqlem2  14432  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  cvgcmp2nlemabs  14750  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trilpo  14761  redcwlpo  14773  nconstwlpolemgt0  14781  nconstwlpo  14783  neapmkv  14785