Theorem oveq12i 7382

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵
oveq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
oveq12i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		oveq12 7379	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1542  (class class class)co 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  oveq123i  7384  caovdir  7604  caovdilem  7605  caovlem2  7606  cnfcom2  9625  canthwelem  10575  adderpqlem  10879  addassnq  10883  distrnq  10886  ltanq  10896  1lt2nq  10898  ltexnq  10900  halfnq  10901  mulcmpblnrlem  10995  mulcomsr  11014  distrsr  11016  m1p1sr  11017  m1m1sr  11018  mulgt0sr  11030  addcnsrec  11068  mulcnsrec  11069  axmulcom  11080  axmulass  11082  axdistr  11083  axi2m1  11084  addrid  11327  3t3e9  12321  8th4div3  12375  halfthird  12376  numma  12665  decmul10add  12690  4t3lem  12718  9t11e99  12751  5recm6rec  12764  fz0to3un2pr  13559  seqfeq4  13988  seqof  13996  sqdivi  14122  sq4e2t8  14136  i4  14141  binom2i  14149  nn0opthlem1  14205  facp1  14215  fac2  14216  fac3  14217  fac4  14218  faclbnd4lem1  14230  4bc2eq6  14266  ccat2s1len  14561  ccat2s1p2  14568  cats1len  14797  cats2cat  14799  ofs2  14908  cji  15096  01sqrexlem5  15183  fsumadd  15677  fsumsplitf  15679  fsumsplitsnun  15692  0.999...  15818  fprodmul  15897  fproddiv  15898  fprodsplitf  15925  bpoly3  15995  fsumcube  15997  efsep  16049  ef01bndlem  16123  cos2bnd  16127  rpnnen2lem3  16155  3dvds2dec  16274  flodddiv4  16356  sadeq  16413  gcdaddmlem  16465  bezout  16484  nn0expgcd  16505  nn0gcdsq  16693  pythagtriplem16  16772  4sqlem19  16905  dec5nprm  17008  dec2nprm  17009  mod2xnegi  17013  numexp2x  17020  decsplit  17024  karatsuba  17025  2exp5  17027  2exp11  17031  2exp16  17032  37prm  17062  43prm  17063  83prm  17064  139prm  17065  163prm  17066  317prm  17067  631prm  17068  1259lem1  17072  1259lem2  17073  1259lem3  17074  1259lem4  17075  1259lem5  17076  1259prm  17077  2503lem1  17078  2503lem2  17079  2503lem3  17080  2503prm  17081  4001lem1  17082  4001lem2  17083  4001lem3  17084  4001lem4  17085  4001prm  17086  funcoppc  17813  estrchom  18064  funcestrcsetclem5  18081  yonedalem3b  18216  ecqusaddd  19138  symgressbas  19328  gsum2dlem2  19917  gsumle  20091  opprrng  20298  isrhm  20431  rngqiprnglinlem2  21264  pzriprng1ALT  21468  evlsval  22058  mamudi  22364  mamudir  22365  oftpos  22413  mamutpos  22419  mdetrlin  22563  mdetrlin2  22568  mdetunilem5  22577  cpmadugsumfi  22838  cnmpt2res  23638  ussval  24220  icopnfhmeo  24914  iccpnfhmeo  24916  pcoass  24997  ovolunlem1a  25470  ioombl1lem3  25534  ioombl1lem4  25535  mbfimaopnlem  25629  itgfsum  25801  iblabslem  25802  itgsplit  25810  dveflem  25956  efhalfpi  26453  efipi  26455  sin2pi  26457  ef2pi  26459  sincosq3sgn  26482  sincosq4sgn  26483  sinq34lt0t  26491  sincos4thpi  26495  tan4thpi  26496  tan4thpiOLD  26497  sincos6thpi  26498  sincos3rdpi  26499  pigt3  26500  pige3ALT  26502  cxpcn3  26731  lawcos  26799  1cubrlem  26824  quart1lem  26838  quart1  26839  asin1  26877  atancj  26893  atanlogsublem  26898  log2cnv  26927  log2tlbnd  26928  log2ublem3  26931  log2ub  26932  birthday  26937  basellem8  27071  basellem9  27072  cht2  27155  cht3  27156  1sgm2ppw  27184  bclbnd  27264  bposlem8  27275  bposlem9  27276  lgsdi  27318  lgsquadlem1  27364  2lgsoddprmlem3c  27396  2lgsoddprmlem3d  27397  addsqnreup  27427  addsval2  27976  addsunif  28015  addsasslem1  28016  addsasslem2  28017  negsval  28038  neg0s  28039  neg1s  28040  negsid  28054  mulsval2  28124  muls01  28125  mulsproplem2  28130  mulsproplem3  28131  mulsproplem4  28132  mulsproplem5  28133  mulsproplem6  28134  mulsproplem7  28135  mulsproplem8  28136  mulsproplem12  28140  mulsproplem13  28141  mulsproplem14  28142  mulsunif  28163  addsdilem1  28164  addsdilem2  28165  mulsasslem1  28176  mulsasslem2  28177  mulsunif2  28183  precsexlem11  28230  onmulscl  28291  twocut  28436  mirauto  28774  axsegconlem9  29016  ax5seglem7  29026  vtxdginducedm1  29635  clwlkclwwlkfo  30102  eupth2eucrct  30310  ex-exp  30543  ex-fac  30544  ex-bc  30545  ex-hash  30546  ip0i  30919  ip1ilem  30920  ip2i  30922  ipdirilem  30923  ipasslem10  30933  ip2dii  30938  pythi  30944  siilem1  30945  hvsubsub4i  31153  hvsubcan2i  31158  hisubcomi  31198  normlem0  31203  normlem1  31204  normlem2  31205  normlem3  31206  normlem6  31209  normlem8  31211  normlem9  31212  bcseqi  31214  norm-ii-i  31231  norm-iii-i  31233  normpythi  31236  norm3difi  31241  normpari  31248  normpar2i  31250  polid2i  31251  polidi  31252  bcsiALT  31273  lediri  31631  h1de2i  31647  cmcmlem  31685  cmbr2i  31690  cm2j  31714  fh3i  31717  fh4i  31718  pjaddii  31769  pjsslem  31773  pjssmii  31775  pjdifnormii  31777  lnopeq0lem1  32099  lnopunilem1  32104  lnophmlem2  32111  pjsdi2i  32251  pjclem1  32289  golem1  32365  dpmul100  32995  dpmul1000  32997  dpadd2  33008  dpadd  33009  dpadd3  33010  dpmul  33011  dpmul4  33012  ccatws1f1o  33050  elrgspnlem2  33343  matdim  33799  fldext2chn  33912  constrextdg2lem  33932  constrext2chnlem  33934  iconstr  33950  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  rmulccn  34112  raddcn  34113  xrmulc1cn  34114  xrge0iifhmeo  34120  qqh0  34168  qqh1  34169  elmbfmvol2  34451  mbfmcnt  34452  eulerpartlemgvv  34560  eulerpartlemgh  34562  fib2  34586  fib3  34587  fib4  34588  fib5  34589  fib6  34590  ballotlem2  34673  ballotlemfval0  34680  ballotth  34722  hgt750lem2  34836  problem2  35888  problem4  35890  quad3  35892  ditgeq123i  36431  cbvditgvw2  36471  poimirlem30  37930  iblabsnclem  37963  dalem10  40078  cdleme0e  40622  cdleme7c  40650  cdleme20c  40716  3exp7  42452  3lexlogpow5ineq1  42453  3lexlogpow5ineq5  42459  aks4d1p1  42475  5bc2eq10  42541  aks5lem3a  42588  sn-1ne2  42664  sqmid3api  42682  sqdeccom12  42688  sq3deccom12  42689  tan3rdpi  42751  sin2t3rdpi  42752  cos2t3rdpi  42753  rei4  42823  ipiiie0  42837  sn-0tie0  42850  mzpcompact2lem  43137  pellexlem5  43219  pellfundgt1  43269  jm2.27c  43393  areaquad  43602  resqrtvalex  44030  imsqrtvalex  44031  lhe4.4ex1a  44714  mccl  45987  dvnprodlem2  46334  itgsin0pilem1  46337  stoweidlem13  46400  wallispilem4  46455  wallispi2lem1  46458  wallispi2lem2  46459  dirkerper  46483  dirkertrigeqlem1  46485  fourierdlem30  46524  fourierdlem47  46540  fourierdlem103  46596  fourierdlem104  46597  fouriersw  46618  etransclem37  46658  sge0splitmpt  46798  sge0xaddlem2  46821  sge0xadd  46822  caragen0  46893  caragenuncllem  46899  nthrucw  47273  fsumsplitsndif  47762  139prmALT  47985  127prm  47988  m11nprm  47990  3exp4mod41  48005  sbgoldbo  48176  2t6m3t4e0  48737  lincsum  48818  zlmodzxzequa  48885  zlmodzxzequap  48888  zlmodzxzldeplem3  48891  rrx2linest  49131  line2  49141  itsclc0yqsollem1  49151  itsclquadb  49165  itscnhlinecirc02plem2  49172  postcofval  49752  postcofcl  49753  precofval  49755  precofvalALT  49756  precofcl  49758  termcfuncval  49920