Theorem oveq12d 5888

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

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

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 3809  df-br 4002  df-iota 5175  df-fv 5221  df-ov 5873

This theorem is referenced by:  oveq123d  5891  ovmpodxf  5995  ovmpodf  6001  caovdig  6044  caovdir2d  6046  caovdirg  6047  caovdilemd  6061  caovlem2d  6062  offval  6085  ofvalg  6087  offval2  6093  ofco  6096  caofinvl  6100  offres  6131  nnmsucr  6484  nndir  6486  ecovdi  6641  ecovidi  6642  dfplpq2  7348  dfmpq2  7349  addcmpblnq  7361  mulpipqqs  7367  addassnqg  7376  distrnqg  7381  ltaddnq  7401  halfnqq  7404  enq0tr  7428  addcmpblnq0  7437  addnq0mo  7441  addnnnq0  7443  nqnq0a  7448  distrnq0  7453  addassnq0  7456  distnq0r  7457  nq02m  7459  ltexpri  7607  cauappcvgprlemm  7639  cauappcvgprlemloc  7646  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem1  7653  cauappcvgprlem2  7654  cauappcvgprlemlim  7655  cauappcvgpr  7656  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemmu  7689  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexbt  7700  caucvgprprlem2  7704  mulcmpblnrlemg  7734  mulsrmo  7738  mulsrpr  7740  mulcomsrg  7751  distrsrg  7753  recexgt0sr  7767  mulgt0sr  7772  mulextsr1lem  7774  caucvgsrlemgt1  7789  caucvgsr  7796  addcnsr  7828  mulcnsr  7829  recidpirqlemcalc  7851  axaddcl  7858  axmulcl  7860  axmulcom  7865  axmulass  7867  axdistr  7868  axcaucvglemcau  7892  axcaucvglemres  7893  adddir  7943  muladd11  8084  1p1times  8085  muladd11r  8107  pnpcan2  8191  muladd  8335  subdir  8337  mulsub  8352  mulreim  8555  apadd1  8559  mulext1  8563  recextlem1  8602  muleqadd  8619  divdirap  8648  divadddivap  8678  conjmulap  8680  divcanap5rd  8769  subrecap  8790  xp1d2m1eqxm1d2  9165  div4p1lem1div2  9166  cnref1o  9644  xnegid  9853  xposdif  9876  xleaddadd  9881  icoshftf1o  9985  lincmb01cmp  9997  iccf1o  9998  fz01en  10046  fzrev3  10080  fzrevral2  10099  fzrevral3  10100  fzshftral  10101  fzoaddel2  10186  fzosubel  10187  fzosubel2  10188  fzocatel  10192  modqsubdir  10386  addmodlteq  10391  frecuzrdgsuc  10407  frecfzen2  10420  iseqovex  10449  seqvalcd  10452  seq3caopr3  10474  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  seq3id3  10500  seqfeq3  10505  seq3distr  10506  ser3le  10511  mulexp  10552  mulexpzap  10553  expaddzap  10557  expubnd  10570  subsq  10619  binom2  10624  binom21  10625  binom2sub  10626  binom2sub1  10627  binom3  10630  sqoddm1div8  10666  nn0opthlem1d  10691  nn0opthd  10693  facp1  10701  facubnd  10716  bcval  10720  bcn1  10729  bcm1k  10731  bcp1n  10732  bcp1nk  10733  bcval5  10734  bcn2  10735  bcpasc  10737  hashun  10776  hashfz  10792  crre  10857  replim  10859  remullem  10871  remul2  10873  immul2  10880  cjcj  10883  cjadd  10884  ipcnval  10886  cjmulval  10888  cjneg  10890  imval2  10894  cjreim  10903  cvg1nlemcau  10984  cvg1nlemres  10985  resqrexlemp1rp  11006  resqrexlemfp1  11009  resqrexlemcalc1  11014  resqrexlemcalc2  11015  resqrex  11026  sqabsadd  11055  sqabssub  11056  absreimsq  11067  recan  11109  amgm2  11118  maxabslemab  11206  maxabslemval  11208  max0addsup  11219  minabs  11235  bdtrilem  11238  bdtri  11239  xrmaxadd  11260  xrminadd  11274  xrbdtri  11275  subcn2  11310  reccn2ap  11312  climle  11333  climcvg1nlem  11348  serf0  11351  fsumadd  11405  fsumsplit  11406  sumpr  11412  sumtp  11413  isumadd  11430  sumsplitdc  11431  fsum2dlemstep  11433  fsumshftm  11444  fisumrev2  11445  fsumconst  11453  modfsummodlemstep  11456  telfsumo  11465  fsumparts  11469  binomlem  11482  binom  11483  binom1dif  11486  bcxmaslem1  11487  isumsplit  11490  isumnn0nn  11492  arisum  11497  arisum2  11498  trireciplem  11499  trirecip  11500  geosergap  11505  geo2sum  11513  geo2sum2  11514  cvgratnnlemsumlt  11527  mertenslemi1  11534  mertensabs  11536  fprodmul  11590  fprodsplitdc  11595  fprodabs  11615  fprod2dlemstep  11621  fproddivapf  11630  eftabs  11655  eftvalcn  11656  efcllemp  11657  ege2le3  11670  efcj  11672  efaddlem  11673  efsep  11690  ef4p  11693  efgt1p2  11694  efgt1p  11695  sinval  11701  cosval  11702  tanvalap  11707  tanval2ap  11712  tanval3ap  11713  efi4p  11716  sinneg  11725  cosneg  11726  tannegap  11727  efival  11731  efmival  11732  sinadd  11735  cosadd  11736  tanaddaplem  11737  tanaddap  11738  sinsub  11739  cossub  11740  addsin  11741  subsin  11742  sinmul  11743  cosmul  11744  addcos  11745  subcos  11746  sincossq  11747  cos2t  11749  sin01bnd  11756  cos01bnd  11757  efieq1re  11770  demoivreALT  11772  dvds2ln  11822  odd2np1lem  11867  gcdaddm  11975  bezoutlemnewy  11987  dfgcd3  12001  dvdsgcd  12003  mulgcd  12007  mulgcdr  12009  gcddiv  12010  sqgcd  12020  lcmgcdlem  12067  lcmgcd  12068  qredeu  12087  divgcdcoprm0  12091  cncongr1  12093  oddpwdclemdc  12163  sqrt2irraplemnn  12169  qnumdenbi  12182  zgcdsq  12191  hashdvds  12211  phiprmpw  12212  phimullem  12215  eulerthlema  12220  prmdiv  12225  modprm0  12244  coprimeprodsq  12247  pythagtriplem1  12255  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem15  12268  pythagtriplem16  12269  pythagtriplem17  12270  pythagtriplem19  12272  pcval  12286  pcmul  12291  pcdiv  12292  pcqmul  12293  pcid  12313  pcaddlem  12328  pcmpt  12331  pcmpt2  12332  pcmptdvds  12333  pcbc  12339  4sqlem4  12380  mul4sqlem  12381  mul4sq  12382  ennnfonelemp1  12397  nninfdclemp1  12441  ressvalsets  12514  topnvalg  12686  topnpropgd  12688  ismhm  12781  mhmf1o  12789  0mhm  12801  mhmco  12802  mhmeql  12804  isgrpid2  12841  grpnpcan  12890  mhmmnd  12908  mulgnndir  12939  mulgdir  12942  ablsub4  13016  mgpvalg  13033  mgptopng  13039  mgpress  13041  srglmhm  13076  srgrmhm  13077  rngo2times  13111  ringcom  13114  ringpropd  13117  ring1  13136  opprvalg  13140  opprring  13148  invrfvald  13190  dvrvald  13202  dvrdir  13211  rdivmuldivd  13212  cnfval  13476  cnpfval  13477  ispsmet  13605  psmet0  13609  psmettri2  13610  psmetres2  13615  ismet  13626  isxmet  13627  xmettri2  13643  xmetres2  13661  xblss2  13687  xmstri2  13752  mstri2  13753  xmstri  13754  mstri  13755  xmstri3  13756  mstri3  13757  msrtri  13758  comet  13781  bdxmet  13783  txmetcnp  13800  metcnpd  13802  cnmet  13812  ioo2bl  13825  fsumcncntop  13838  elcncf  13842  mulc1cncf  13858  cncfco  13860  cncfcncntop  13862  cncfmptc  13864  cncfmptid  13865  addccncf  13868  cdivcncfap  13869  negcncf  13870  mulcncflem  13872  limccnp2cntop  13928  reldvg  13930  dvfvalap  13932  eldvap  13933  dvconst  13943  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  dvcjbr  13954  dvexp  13957  dvrecap  13959  dveflem  13969  dvef  13970  sinperlem  14011  sinmpi  14018  cosmpi  14019  sinppi  14020  cosppi  14021  efimpi  14022  sinhalfpip  14023  sinhalfpim  14024  coshalfpip  14025  coshalfpim  14026  ptolemy  14027  tangtx  14041  logdivlti  14084  rpcxpadd  14108  rpmulcxp  14112  rplogbchbase  14150  rprelogbmul  14155  binom4  14179  lgsval  14187  lgsfvalg  14188  lgsval2lem  14193  lgsval4a  14205  lgsneg  14207  lgsdilem  14210  lgsdirprm  14217  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  2sqlem2  14233  2sqlem3  14235  2sqlem4  14236  2sqlem8  14241  cvgcmp2nlemabs  14551  trilpolemclim  14555  trilpolemcl  14556  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560  trilpo  14562  redcwlpo  14574  nconstwlpolemgt0  14582  nconstwlpo  14584  neapmkv  14586