Theorem oveq12d 6103

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123d  6106  ovmpodxf  6214  ovmpodf  6220  caovdig  6264  caovdir2d  6266  caovdirg  6267  caovdilemd  6281  caovlem2d  6282  offval  6310  ofvalg  6312  offval2  6318  ofco  6321  caofinvl  6328  offres  6368  nnmsucr  6761  nndir  6763  ecovdi  6920  ecovidi  6921  dfplpq2  7722  dfmpq2  7723  addcmpblnq  7735  mulpipqqs  7741  addassnqg  7750  distrnqg  7755  ltaddnq  7775  halfnqq  7778  enq0tr  7802  addcmpblnq0  7811  addnq0mo  7815  addnnnq0  7817  nqnq0a  7822  distrnq0  7827  addassnq0  7830  distnq0r  7831  nq02m  7833  ltexpri  7981  cauappcvgprlemm  8013  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemmu  8063  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem2  8078  mulcmpblnrlemg  8108  mulsrmo  8112  mulsrpr  8114  mulcomsrg  8125  distrsrg  8127  recexgt0sr  8141  mulgt0sr  8146  mulextsr1lem  8148  caucvgsrlemgt1  8163  caucvgsr  8170  addcnsr  8202  mulcnsr  8203  recidpirqlemcalc  8225  axaddcl  8232  axmulcl  8234  axmulcom  8239  axmulass  8241  axdistr  8242  axcaucvglemcau  8266  axcaucvglemres  8267  adddir  8318  muladd11  8461  1p1times  8462  muladd11r  8484  pnpcan2  8568  muladd  8713  subdir  8715  mulsub  8730  mulreim  8935  apadd1  8939  mulext1  8943  recextlem1  8982  muleqadd  9001  divdirap  9030  divadddivap  9060  conjmulap  9062  divcanap5rd  9151  subrecap  9172  xp1d2m1eqxm1d2  9563  div4p1lem1div2  9564  cnref1o  10062  xnegid  10272  xposdif  10295  xleaddadd  10300  icoshftf1o  10404  lincmb01cmp  10416  iccf1o  10418  fz01en  10470  fzrev3  10505  fzrevral2  10524  fzrevral3  10525  fzshftral  10526  fzoaddel2  10619  fzosubel  10623  fzosubel2  10624  fzocatel  10628  modqsubdir  10845  addmodlteq  10850  frecuzrdgsuc  10866  frecfzen2  10879  iseqovex  10910  seqvalcd  10913  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seqf1oglem2  10972  seq3id3  10976  seqfeq3  10981  seq3distr  10984  ser3le  10989  mulexp  11030  mulexpzap  11031  expaddzap  11035  expubnd  11048  subsq  11098  binom2  11103  binom21  11104  binom2sub  11105  binom2sub1  11106  binom3  11109  sqoddm1div8  11146  mulsubdivbinom2ap  11165  nn0opthlem1d  11174  nn0opthd  11176  facp1  11184  facubnd  11199  bcval  11203  bcn1  11212  bcm1k  11214  bcp1n  11215  bcp1nk  11216  bcval5  11217  bcn2  11218  bcpasc  11220  bcm1n  11223  hashun  11261  hashfz  11278  hashfibclem  11298  hashfibc  11299  hashf1lem2  11302  hashf1  11303  hashtpgim  11313  ccatlid  11390  ccatass  11392  ccat1st1st  11425  swrdval  11436  swrdspsleq  11455  ccatswrd  11458  pfxval  11462  addlenpfx  11479  ccatpfx  11489  ccatopth  11504  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  swrdccat  11523  swrdccat3blem  11527  swrdccatin2d  11532  pfxccatin12d  11533  cats1lend  11555  cats2catd  11557  s2eqd  11558  s3eqd  11559  s4eqd  11560  s5eqd  11561  s6eqd  11562  s7eqd  11563  s8eqd  11564  crre  11638  replim  11640  remullem  11652  remul2  11654  immul2  11661  cjcj  11664  cjadd  11665  ipcnval  11667  cjmulval  11669  cjneg  11671  imval2  11675  cjreim  11685  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrex  11808  sqabsadd  11837  sqabssub  11838  absreimsq  11849  recan  11892  amgm2  11901  maxabslemab  11989  maxabslemval  11991  max0addsup  12002  minabs  12020  bdtrilem  12024  bdtri  12025  xrmaxadd  12046  xrminadd  12060  xrbdtri  12061  subcn2  12096  reccn2ap  12098  climle  12119  climcvg1nlem  12134  serf0  12137  fsumadd  12192  fsumsplit  12193  sumpr  12199  sumtp  12200  isumadd  12217  sumsplitdc  12218  fsum2dlemstep  12220  fsumshftm  12231  fisumrev2  12232  fsumconst  12240  modfsummodlemstep  12243  telfsumo  12252  fsumparts  12256  binomlem  12269  binom  12270  binom1dif  12273  bcxmaslem1  12274  isumsplit  12277  isumnn0nn  12279  arisum  12284  arisum2  12285  trireciplem  12286  trirecip  12287  geosergap  12292  geo2sum  12300  geo2sum2  12301  cvgratnnlemsumlt  12314  mertenslemi1  12321  mertensabs  12323  fprodmul  12377  fprodsplitdc  12382  fprodabs  12402  fprod2dlemstep  12408  fproddivapf  12417  eftabs  12442  eftvalcn  12443  efcllemp  12444  ege2le3  12457  efcj  12459  efaddlem  12460  efsep  12477  ef4p  12480  efgt1p2  12481  efgt1p  12482  sinval  12488  cosval  12489  tanvalap  12494  tanval2ap  12499  tanval3ap  12500  efi4p  12503  sinneg  12512  cosneg  12513  tannegap  12514  efival  12518  efmival  12519  sinadd  12522  cosadd  12523  tanaddaplem  12524  tanaddap  12525  sinsub  12526  cossub  12527  addsin  12528  subsin  12529  sinmul  12530  cosmul  12531  addcos  12532  subcos  12533  sincossq  12534  cos2t  12536  sin01bnd  12543  cos01bnd  12544  efieq1re  12558  demoivreALT  12560  dvds2ln  12610  odd2np1lem  12658  bitsinv1lem  12747  gcdaddm  12780  bezoutlemnewy  12792  dfgcd3  12806  dvdsgcd  12808  mulgcd  12812  mulgcdr  12814  gcddiv  12815  sqgcd  12825  lcmgcdlem  12874  lcmgcd  12875  qredeu  12894  divgcdcoprm0  12898  cncongr1  12900  nnmaxpwlemparts  12971  sqrt2irraplemnn  12978  qnumdenbi  12991  zgcdsq  13000  hashdvds  13022  phiprmpw  13023  phimullem  13026  eulerthlema  13031  prmdiv  13036  modprm0  13056  coprimeprodsq  13059  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem19  13084  pcval  13098  pcmul  13103  pcdiv  13104  pcqmul  13105  pcid  13126  pcaddlem  13141  pcmpt  13145  pcmpt2  13146  pcmptdvds  13147  pcbc  13153  4sqlem4  13194  mul4sqlem  13195  mul4sq  13196  4sqlem11  13203  4sqlem12  13204  4sqlem15  13207  4sqlem17  13209  ballotfilemfval  13281  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfmpn  13286  ballotfilemgval  13319  ballotfilemgun  13320  ballotfilemfrc  13322  ballotfilemfrceq  13324  ennnfonelemp1  13349  nninfdclemp1  13393  ressvalsets  13470  topnvalg  13658  topnpropgd  13660  qusval  13697  qusex  13699  qusaddvallemg  13707  imasmnd2  13812  ismhm  13821  mhmf1o  13830  0mhm  13846  mhmco  13850  mhmeql  13852  isgrpid2  13898  grpnpcan  13950  imasgrp2  13966  mhmmnd  13972  mulgnndir  14007  mulgdir  14010  isnsg3  14063  isghm  14099  ghmnsgima  14124  ghmf1o  14131  conjghm  14132  qusghm  14138  ablsub4  14201  ghmcmn  14215  invghm  14217  gzsumconst  14227  gzsumgsum  14239  gsump1  14241  gsumzfi  14242  gsummptfidmadd  14245  gsumconstcmn  14250  prdsex  14256  prdsval  14257  xpsval  14285  pwsval  14288  mgpvalg  14304  mgptopng  14312  mgpress  14314  rngdi  14323  rngdir  14324  rngpropd  14338  imasrng  14339  srglmhm  14381  srgrmhm  14382  ringo2times  14417  ringcom  14420  ringpropd  14427  ring1  14448  ringlghm  14450  ringrghm  14451  imasring  14453  opprvalg  14458  opprrng  14466  opprring  14468  invrfvald  14513  dvrvald  14525  dvrdir  14534  rdivmuldivd  14535  islmod  14711  lmodlema  14712  islmodd  14713  lmodcom  14754  lmodnegadd  14757  lmodprop2d  14769  rmodislmod  14772  lsssn0  14791  sraval  14858  qusrhm  14949  gsumfsum  15007  expghmap  15026  mulgghm2  15027  mulgrhm  15028  zlmval  15046  znval  15055  asclghm  15109  assamulgscmlem1  15125  assamulgscm  15127  psrval  15134  mplvalcoe  15172  cnfval  15386  cnpfval  15387  ispsmet  15515  psmet0  15519  psmettri2  15520  psmetres2  15525  ismet  15536  isxmet  15537  xmettri2  15553  xmetres2  15571  xblss2  15597  xmstri2  15662  mstri2  15663  xmstri  15664  mstri  15665  xmstri3  15666  mstri3  15667  msrtri  15668  comet  15691  bdxmet  15693  txmetcnp  15710  metcnpd  15712  cnmet  15722  ioo2bl  15743  mpomulcn  15758  fsumcncntop  15759  elcncf  15765  mulc1cncf  15781  cncfco  15783  cncfcncntop  15785  cncfmptc  15788  cncfmptid  15789  addccncf  15792  cdivcncfap  15796  negcncf  15797  mulcncflem  15799  limccnp2cntop  15869  reldvg  15871  dvfvalap  15873  eldvap  15874  dvconst  15886  dvconstre  15888  dvconstss  15890  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvexp  15903  dvrecap  15905  dvmptid  15908  dvmptc  15909  dveflem  15918  dvef  15919  elplyd  15933  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plyadd  15943  plymul  15944  plycoeid3  15949  plycolemc  15950  plyco  15951  plycjlemc  15952  plycj  15953  plyrecj  15955  dvply1  15957  dvply2g  15958  sinperlem  16001  sinmpi  16008  cosmpi  16009  sinppi  16010  cosppi  16011  efimpi  16012  sinhalfpip  16013  sinhalfpim  16014  coshalfpip  16015  coshalfpim  16016  ptolemy  16017  tangtx  16031  logdivlti  16075  rpcxpadd  16102  rpmulcxp  16106  rplogbchbase  16147  rprelogbmul  16152  binom4  16180  log2tlbndlog2  16181  log2ublem2  16183  birthdaylem2  16187  pellexlem2  16191  pellexlem3  16192  wilthlem1  16193  chtprm  16222  chtdif  16225  efchtqdvds  16226  ppidif  16230  1sgmprm  16249  1sgm2ppw  16250  sgmmul  16251  ppiqub  16254  chtublem  16256  chtqub  16257  mersenne  16258  perfect1  16259  perfectlem2  16261  perfect  16262  bcmono  16265  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  bposlem2  16273  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsval4a  16307  lgsneg  16309  lgsdilem  16312  lgsdirprm  16319  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  gausslemma2dlem4  16349  gausslemma2dlem6  16352  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem1  16366  lgsquad2lem2  16367  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2sqlem2  16400  2sqlem3  16402  2sqlem4  16403  2sqlem8  16408  vtxdgfval  16695  vtxdgfifival  16698  vtxdgop  16699  vtxdgfi0e  16702  vtxdeqd  16703  vtxdfifiun  16704  vtxduspgrfvedgfi  16708  1loopgrvd2fi  16712  repiecele0  17241  repiecege0  17242  repiecef  17243  cvgcmp2nlemabs  17247  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trilpo  17259  redcwlpo  17272  nconstwlpolemgt0  17281  nconstwlpo  17283  neapmkv  17285