Theorem oveq12d 6106

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

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

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq123d  6109  ovmpodxf  6217  ovmpodf  6223  caovdig  6267  caovdir2d  6269  caovdirg  6270  caovdilemd  6284  caovlem2d  6285  offval  6314  ofvalg  6316  offval2  6322  ofco  6325  caofinvl  6332  offres  6372  nnmsucr  6766  nndir  6768  ecovdi  6925  ecovidi  6926  dfplpq2  7727  dfmpq2  7728  addcmpblnq  7740  mulpipqqs  7746  addassnqg  7755  distrnqg  7760  ltaddnq  7780  halfnqq  7783  enq0tr  7807  addcmpblnq0  7816  addnq0mo  7820  addnnnq0  7822  nqnq0a  7827  distrnq0  7832  addassnq0  7835  distnq0r  7836  nq02m  7838  ltexpri  7986  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemmu  8068  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  caucvgprprlem2  8083  mulcmpblnrlemg  8113  mulsrmo  8117  mulsrpr  8119  mulcomsrg  8130  distrsrg  8132  recexgt0sr  8146  mulgt0sr  8151  mulextsr1lem  8153  caucvgsrlemgt1  8168  caucvgsr  8175  addcnsr  8207  mulcnsr  8208  recidpirqlemcalc  8230  axaddcl  8237  axmulcl  8239  axmulcom  8244  axmulass  8246  axdistr  8247  axcaucvglemcau  8271  axcaucvglemres  8272  adddir  8323  muladd11  8466  1p1times  8467  muladd11r  8489  pnpcan2  8573  muladd  8718  subdir  8720  mulsub  8735  mulreim  8940  apadd1  8944  mulext1  8948  recextlem1  8987  muleqadd  9006  divdirap  9035  divadddivap  9065  conjmulap  9067  divcanap5rd  9156  subrecap  9177  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  cnref1o  10067  xnegid  10277  xposdif  10300  xleaddadd  10305  icoshftf1o  10409  lincmb01cmp  10421  iccf1o  10423  fz01en  10475  fzrev3  10510  fzrevral2  10529  fzrevral3  10530  fzshftral  10531  fzoaddel2  10624  fzosubel  10628  fzosubel2  10629  fzocatel  10633  modqsubdir  10850  addmodlteq  10855  frecuzrdgsuc  10871  frecfzen2  10884  iseqovex  10915  seqvalcd  10918  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seqf1oglem2  10977  seq3id3  10981  seqfeq3  10986  seq3distr  10989  ser3le  10994  mulexp  11035  mulexpzap  11036  expaddzap  11040  expubnd  11053  subsq  11103  binom2  11108  binom21  11109  binom2sub  11110  binom2sub1  11111  binom3  11114  sqoddm1div8  11151  mulsubdivbinom2ap  11170  nn0opthlem1d  11179  nn0opthd  11181  facp1  11189  facubnd  11204  bcval  11208  bcn1  11217  bcm1k  11219  bcp1n  11220  bcp1nk  11221  bcval5  11222  bcn2  11223  bcpasc  11225  bcm1n  11228  hashun  11266  hashfz  11283  hashfibclem  11303  hashfibc  11304  hashf1lem2  11307  hashf1  11308  hashtpgim  11318  ccatlid  11395  ccatass  11397  ccat1st1st  11430  swrdval  11441  swrdspsleq  11460  ccatswrd  11463  pfxval  11467  addlenpfx  11484  ccatpfx  11494  ccatopth  11509  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  swrdccat  11528  swrdccat3blem  11532  swrdccatin2d  11537  pfxccatin12d  11538  cats1lend  11560  cats2catd  11562  s2eqd  11563  s3eqd  11564  s4eqd  11565  s5eqd  11566  s6eqd  11567  s7eqd  11568  s8eqd  11569  crre  11643  replim  11645  remullem  11657  remul2  11659  immul2  11666  cjcj  11669  cjadd  11670  ipcnval  11672  cjmulval  11674  cjneg  11676  imval2  11680  cjreim  11690  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrex  11813  sqabsadd  11842  sqabssub  11843  absreimsq  11854  recan  11897  amgm2  11906  maxabslemab  11994  maxabslemval  11996  max0addsup  12007  minabs  12025  bdtrilem  12029  bdtri  12030  xrmaxadd  12051  xrminadd  12065  xrbdtri  12066  subcn2  12101  reccn2ap  12103  climle  12124  climcvg1nlem  12139  serf0  12142  fsumadd  12197  fsumsplit  12198  sumpr  12204  sumtp  12205  isumadd  12222  sumsplitdc  12223  fsum2dlemstep  12225  fsumshftm  12236  fisumrev2  12237  fsumconst  12245  modfsummodlemstep  12248  telfsumo  12257  fsumparts  12261  binomlem  12274  binom  12275  binom1dif  12278  bcxmaslem1  12279  isumsplit  12282  isumnn0nn  12284  arisum  12289  arisum2  12290  trireciplem  12291  trirecip  12292  geosergap  12297  geo2sum  12305  geo2sum2  12306  cvgratnnlemsumlt  12319  mertenslemi1  12326  mertensabs  12328  fprodmul  12382  fprodsplitdc  12387  fprodabs  12407  fprod2dlemstep  12413  fproddivapf  12422  eftabs  12447  eftvalcn  12448  efcllemp  12449  ege2le3  12462  efcj  12464  efaddlem  12465  efsep  12482  ef4p  12485  efgt1p2  12486  efgt1p  12487  sinval  12493  cosval  12494  tanvalap  12499  tanval2ap  12504  tanval3ap  12505  efi4p  12508  sinneg  12517  cosneg  12518  tannegap  12519  efival  12523  efmival  12524  sinadd  12527  cosadd  12528  tanaddaplem  12529  tanaddap  12530  sinsub  12531  cossub  12532  addsin  12533  subsin  12534  sinmul  12535  cosmul  12536  addcos  12537  subcos  12538  sincossq  12539  cos2t  12541  sin01bnd  12548  cos01bnd  12549  efieq1re  12563  demoivreALT  12565  dvds2ln  12615  odd2np1lem  12663  bitsinv1lem  12752  gcdaddm  12785  bezoutlemnewy  12797  dfgcd3  12811  dvdsgcd  12813  mulgcd  12817  mulgcdr  12819  gcddiv  12820  sqgcd  12830  lcmgcdlem  12879  lcmgcd  12880  qredeu  12899  divgcdcoprm0  12903  cncongr1  12905  nnmaxpwlemparts  12976  sqrt2irraplemnn  12983  qnumdenbi  12996  zgcdsq  13005  hashdvds  13027  phiprmpw  13028  phimullem  13031  eulerthlema  13036  prmdiv  13041  modprm0  13061  coprimeprodsq  13064  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  pythagtriplem19  13089  pcval  13103  pcmul  13108  pcdiv  13109  pcqmul  13110  pcid  13131  pcaddlem  13146  pcmpt  13150  pcmpt2  13151  pcmptdvds  13152  pcbc  13158  4sqlem4  13199  mul4sqlem  13200  mul4sq  13201  4sqlem11  13208  4sqlem12  13209  4sqlem15  13212  4sqlem17  13214  ballotfilemfval  13286  ballotfilemfp1  13288  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfmpn  13291  ballotfilemgval  13324  ballotfilemgun  13325  ballotfilemfrc  13327  ballotfilemfrceq  13329  ennnfonelemp1  13354  nninfdclemp1  13398  ressvalsets  13475  topnvalg  13663  topnpropgd  13665  qusval  13702  qusex  13704  qusaddvallemg  13712  imasmnd2  13817  ismhm  13826  mhmf1o  13835  0mhm  13851  mhmco  13855  mhmeql  13857  isgrpid2  13903  grpnpcan  13955  imasgrp2  13971  mhmmnd  13977  mulgnndir  14012  mulgdir  14015  isnsg3  14068  isghm  14104  ghmnsgima  14129  ghmf1o  14136  conjghm  14137  qusghm  14143  ablsub4  14206  ghmcmn  14220  invghm  14222  gzsumconst  14232  gzsumgsum  14244  gsump1  14246  gsumzfi  14247  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsummptfidmsplitres  14254  gsumsplitfi  14255  gsumsnfdcmn  14256  gsumconstcmn  14265  prdsex  14278  prdsval  14279  xpsval  14307  pwsval  14310  mgpvalg  14326  mgptopng  14334  mgpress  14336  rngdi  14345  rngdir  14346  rngpropd  14360  imasrng  14361  srglmhm  14403  srgrmhm  14404  ringo2times  14439  ringcom  14442  ringpropd  14449  ring1  14470  ringlghm  14472  ringrghm  14473  imasring  14477  opprvalg  14482  opprrng  14490  opprring  14492  invrfvald  14537  dvrvald  14549  dvrdir  14558  rdivmuldivd  14559  islmod  14735  lmodlema  14736  islmodd  14737  lmodcom  14778  lmodnegadd  14781  lmodprop2d  14793  rmodislmod  14796  lsssn0  14815  sraval  14882  qusrhm  14973  gsumfsum  15031  expghmap  15050  mulgghm2  15051  mulgrhm  15052  zlmval  15070  znval  15079  asclghm  15133  assamulgscmlem1  15149  assamulgscm  15151  psrval  15160  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  mplvalg  15222  mplsubgfilemcl  15232  cnfval  15437  cnpfval  15438  ispsmet  15566  psmet0  15570  psmettri2  15571  psmetres2  15576  ismet  15587  isxmet  15588  xmettri2  15604  xmetres2  15622  xblss2  15648  xmstri2  15713  mstri2  15714  xmstri  15715  mstri  15716  xmstri3  15717  mstri3  15718  msrtri  15719  comet  15742  bdxmet  15744  txmetcnp  15761  metcnpd  15763  cnmet  15773  ioo2bl  15794  mpomulcn  15809  fsumcncntop  15810  elcncf  15816  mulc1cncf  15832  cncfco  15834  cncfcncntop  15836  cncfmptc  15839  cncfmptid  15840  addccncf  15843  cdivcncfap  15847  negcncf  15848  mulcncflem  15850  limccnp2cntop  15920  reldvg  15922  dvfvalap  15924  eldvap  15925  dvconst  15937  dvconstre  15939  dvconstss  15941  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvexp  15954  dvrecap  15956  dvmptid  15959  dvmptc  15960  dveflem  15969  dvef  15970  elplyd  15984  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plyadd  15994  plymul  15995  plycoeid3  16000  plycolemc  16001  plyco  16002  plycjlemc  16003  plycj  16004  plyrecj  16006  dvply1  16008  dvply2g  16009  sinperlem  16052  sinmpi  16059  cosmpi  16060  sinppi  16061  cosppi  16062  efimpi  16063  sinhalfpip  16064  sinhalfpim  16065  coshalfpip  16066  coshalfpim  16067  ptolemy  16068  tangtx  16082  logdivlti  16128  rpcxpadd  16155  rpmulcxp  16159  efnthr  16193  rplogbchbase  16203  rprelogbmul  16208  binom4  16236  log2tlbndlog2  16237  log2ublem2  16239  birthdaylem2  16243  pellexlem2  16247  pellexlem3  16248  wilthlem1  16249  chtprm  16278  chtdif  16281  efchtqdvds  16282  ppidif  16286  1sgmprm  16305  1sgm2ppw  16306  sgmmul  16307  ppiqub  16310  chtublem  16312  chtqub  16313  mersenne  16314  perfect1  16315  perfectlem2  16317  perfect  16318  bcmono  16321  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsval4a  16363  lgsneg  16365  lgsdilem  16368  lgsdirprm  16375  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  gausslemma2dlem4  16405  gausslemma2dlem6  16408  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  lgsquad2lem2  16423  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2sqlem2  16456  2sqlem3  16458  2sqlem4  16459  2sqlem8  16464  vtxdgfval  16751  vtxdgfifival  16754  vtxdgop  16755  vtxdgfi0e  16758  vtxdeqd  16759  vtxdfifiun  16760  vtxduspgrfvedgfi  16764  1loopgrvd2fi  16768  repiecele0  17298  repiecege0  17299  repiecef  17300  cvgcmp2nlemabs  17304  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trilpo  17316  redcwlpo  17329  nconstwlpolemgt0  17338  nconstwlpo  17340  neapmkv  17342