Theorem oveq12d 6018

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

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6000

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003

This theorem is referenced by:  oveq123d  6021  ovmpodxf  6129  ovmpodf  6135  caovdig  6179  caovdir2d  6181  caovdirg  6182  caovdilemd  6196  caovlem2d  6197  offval  6224  ofvalg  6226  offval2  6232  ofco  6235  caofinvl  6242  offres  6278  nnmsucr  6632  nndir  6634  ecovdi  6791  ecovidi  6792  dfplpq2  7537  dfmpq2  7538  addcmpblnq  7550  mulpipqqs  7556  addassnqg  7565  distrnqg  7570  ltaddnq  7590  halfnqq  7593  enq0tr  7617  addcmpblnq0  7626  addnq0mo  7630  addnnnq0  7632  nqnq0a  7637  distrnq0  7642  addassnq0  7645  distnq0r  7646  nq02m  7648  ltexpri  7796  cauappcvgprlemm  7828  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  cauappcvgprlemlim  7844  cauappcvgpr  7845  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem2  7863  caucvgpr  7865  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemmu  7878  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem2  7893  mulcmpblnrlemg  7923  mulsrmo  7927  mulsrpr  7929  mulcomsrg  7940  distrsrg  7942  recexgt0sr  7956  mulgt0sr  7961  mulextsr1lem  7963  caucvgsrlemgt1  7978  caucvgsr  7985  addcnsr  8017  mulcnsr  8018  recidpirqlemcalc  8040  axaddcl  8047  axmulcl  8049  axmulcom  8054  axmulass  8056  axdistr  8057  axcaucvglemcau  8081  axcaucvglemres  8082  adddir  8133  muladd11  8275  1p1times  8276  muladd11r  8298  pnpcan2  8382  muladd  8526  subdir  8528  mulsub  8543  mulreim  8747  apadd1  8751  mulext1  8755  recextlem1  8794  muleqadd  8811  divdirap  8840  divadddivap  8870  conjmulap  8872  divcanap5rd  8961  subrecap  8982  xp1d2m1eqxm1d2  9360  div4p1lem1div2  9361  cnref1o  9842  xnegid  10051  xposdif  10074  xleaddadd  10079  icoshftf1o  10183  lincmb01cmp  10195  iccf1o  10196  fz01en  10245  fzrev3  10279  fzrevral2  10298  fzrevral3  10299  fzshftral  10300  fzoaddel2  10391  fzosubel  10395  fzosubel2  10396  fzocatel  10400  modqsubdir  10610  addmodlteq  10615  frecuzrdgsuc  10631  frecfzen2  10644  iseqovex  10675  seqvalcd  10678  seq3caopr3  10708  seqcaopr3g  10709  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seqf1oglem2  10737  seq3id3  10741  seqfeq3  10746  seq3distr  10749  ser3le  10754  mulexp  10795  mulexpzap  10796  expaddzap  10800  expubnd  10813  subsq  10863  binom2  10868  binom21  10869  binom2sub  10870  binom2sub1  10871  binom3  10874  sqoddm1div8  10910  mulsubdivbinom2ap  10928  nn0opthlem1d  10937  nn0opthd  10939  facp1  10947  facubnd  10962  bcval  10966  bcn1  10975  bcm1k  10977  bcp1n  10978  bcp1nk  10979  bcval5  10980  bcn2  10981  bcpasc  10983  hashun  11022  hashfz  11038  ccatlid  11136  ccatass  11138  ccat1st1st  11167  swrdval  11175  swrdspsleq  11194  ccatswrd  11197  pfxval  11201  addlenpfx  11218  ccatpfx  11228  ccatopth  11243  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccat  11262  swrdccat3blem  11266  swrdccatin2d  11271  pfxccatin12d  11272  cats1lend  11294  cats2catd  11296  s2eqd  11297  s3eqd  11298  s4eqd  11299  s5eqd  11300  s6eqd  11301  s7eqd  11302  s8eqd  11303  crre  11363  replim  11365  remullem  11377  remul2  11379  immul2  11386  cjcj  11389  cjadd  11390  ipcnval  11392  cjmulval  11394  cjneg  11396  imval2  11400  cjreim  11409  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemp1rp  11512  resqrexlemfp1  11515  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrex  11532  sqabsadd  11561  sqabssub  11562  absreimsq  11573  recan  11615  amgm2  11624  maxabslemab  11712  maxabslemval  11714  max0addsup  11725  minabs  11742  bdtrilem  11745  bdtri  11746  xrmaxadd  11767  xrminadd  11781  xrbdtri  11782  subcn2  11817  reccn2ap  11819  climle  11840  climcvg1nlem  11855  serf0  11858  fsumadd  11912  fsumsplit  11913  sumpr  11919  sumtp  11920  isumadd  11937  sumsplitdc  11938  fsum2dlemstep  11940  fsumshftm  11951  fisumrev2  11952  fsumconst  11960  modfsummodlemstep  11963  telfsumo  11972  fsumparts  11976  binomlem  11989  binom  11990  binom1dif  11993  bcxmaslem1  11994  isumsplit  11997  isumnn0nn  11999  arisum  12004  arisum2  12005  trireciplem  12006  trirecip  12007  geosergap  12012  geo2sum  12020  geo2sum2  12021  cvgratnnlemsumlt  12034  mertenslemi1  12041  mertensabs  12043  fprodmul  12097  fprodsplitdc  12102  fprodabs  12122  fprod2dlemstep  12128  fproddivapf  12137  eftabs  12162  eftvalcn  12163  efcllemp  12164  ege2le3  12177  efcj  12179  efaddlem  12180  efsep  12197  ef4p  12200  efgt1p2  12201  efgt1p  12202  sinval  12208  cosval  12209  tanvalap  12214  tanval2ap  12219  tanval3ap  12220  efi4p  12223  sinneg  12232  cosneg  12233  tannegap  12234  efival  12238  efmival  12239  sinadd  12242  cosadd  12243  tanaddaplem  12244  tanaddap  12245  sinsub  12246  cossub  12247  addsin  12248  subsin  12249  sinmul  12250  cosmul  12251  addcos  12252  subcos  12253  sincossq  12254  cos2t  12256  sin01bnd  12263  cos01bnd  12264  efieq1re  12278  demoivreALT  12280  dvds2ln  12330  odd2np1lem  12378  bitsinv1lem  12467  gcdaddm  12500  bezoutlemnewy  12512  dfgcd3  12526  dvdsgcd  12528  mulgcd  12532  mulgcdr  12534  gcddiv  12535  sqgcd  12545  lcmgcdlem  12594  lcmgcd  12595  qredeu  12614  divgcdcoprm0  12618  cncongr1  12620  oddpwdclemdc  12690  sqrt2irraplemnn  12696  qnumdenbi  12709  zgcdsq  12718  hashdvds  12738  phiprmpw  12739  phimullem  12742  eulerthlema  12747  prmdiv  12752  modprm0  12772  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  pythagtriplem19  12800  pcval  12814  pcmul  12819  pcdiv  12820  pcqmul  12821  pcid  12842  pcaddlem  12857  pcmpt  12861  pcmpt2  12862  pcmptdvds  12863  pcbc  12869  4sqlem4  12910  mul4sqlem  12911  mul4sq  12912  4sqlem11  12919  4sqlem12  12920  4sqlem15  12923  4sqlem17  12925  ennnfonelemp1  12972  nninfdclemp1  13016  ressvalsets  13092  topnvalg  13279  topnpropgd  13281  prdsex  13297  prdsval  13301  pwsval  13319  qusval  13351  qusex  13353  qusaddvallemg  13361  xpsval  13380  gsumprval  13427  imasmnd2  13480  ismhm  13489  mhmf1o  13498  0mhm  13514  mhmco  13518  mhmeql  13520  gsumfzz  13523  isgrpid2  13568  grpnpcan  13620  imasgrp2  13642  mhmmnd  13648  mulgnndir  13683  mulgdir  13686  isnsg3  13739  isghm  13775  ghmnsgima  13800  ghmf1o  13807  conjghm  13808  qusghm  13814  ablsub4  13845  ghmcmn  13859  invghm  13861  gsumfzmptfidmadd  13871  gsumfzconst  13873  mgpvalg  13881  mgptopng  13887  mgpress  13889  rngdi  13898  rngdir  13899  rngpropd  13913  imasrng  13914  srglmhm  13951  srgrmhm  13952  ringo2times  13986  ringcom  13989  ringpropd  13996  ring1  14017  ringlghm  14019  ringrghm  14020  imasring  14022  opprvalg  14027  opprrng  14035  opprring  14037  invrfvald  14080  dvrvald  14092  dvrdir  14101  rdivmuldivd  14102  islmod  14249  lmodlema  14250  islmodd  14251  lmodcom  14291  lmodnegadd  14294  lmodprop2d  14306  rmodislmod  14309  lsssn0  14328  sraval  14395  qusrhm  14486  gsumfzfsumlemm  14545  expghmap  14565  mulgghm2  14566  mulgrhm  14567  zlmval  14585  znval  14594  psrval  14624  mplvalcoe  14648  cnfval  14862  cnpfval  14863  ispsmet  14991  psmet0  14995  psmettri2  14996  psmetres2  15001  ismet  15012  isxmet  15013  xmettri2  15029  xmetres2  15047  xblss2  15073  xmstri2  15138  mstri2  15139  xmstri  15140  mstri  15141  xmstri3  15142  mstri3  15143  msrtri  15144  comet  15167  bdxmet  15169  txmetcnp  15186  metcnpd  15188  cnmet  15198  ioo2bl  15219  mpomulcn  15234  fsumcncntop  15235  elcncf  15241  mulc1cncf  15257  cncfco  15259  cncfcncntop  15261  cncfmptc  15264  cncfmptid  15265  addccncf  15268  cdivcncfap  15272  negcncf  15273  mulcncflem  15275  limccnp2cntop  15345  reldvg  15347  dvfvalap  15349  eldvap  15350  dvconst  15362  dvconstre  15364  dvconstss  15366  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvexp  15379  dvrecap  15381  dvmptid  15384  dvmptc  15385  dveflem  15394  dvef  15395  elplyd  15409  ply1termlem  15410  plyaddlem1  15415  plymullem1  15416  plyadd  15419  plymul  15420  plycoeid3  15425  plycolemc  15426  plyco  15427  plycjlemc  15428  plycj  15429  plyrecj  15431  dvply1  15433  dvply2g  15434  sinperlem  15476  sinmpi  15483  cosmpi  15484  sinppi  15485  cosppi  15486  efimpi  15487  sinhalfpip  15488  sinhalfpim  15489  coshalfpip  15490  coshalfpim  15491  ptolemy  15492  tangtx  15506  logdivlti  15549  rpcxpadd  15573  rpmulcxp  15577  rplogbchbase  15618  rprelogbmul  15623  binom4  15647  wilthlem1  15648  1sgmprm  15662  1sgm2ppw  15663  sgmmul  15664  mersenne  15665  perfect1  15666  perfectlem2  15668  perfect  15669  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsval4a  15695  lgsneg  15697  lgsdilem  15700  lgsdirprm  15707  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  gausslemma2dlem4  15737  gausslemma2dlem6  15740  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  lgsquad2lem2  15755  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2sqlem2  15788  2sqlem3  15790  2sqlem4  15791  2sqlem8  15796  cvgcmp2nlemabs  16359  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trilpo  16370  redcwlpo  16382  nconstwlpolemgt0  16391  nconstwlpo  16393  neapmkv  16395