Theorem oveq12i 7372

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 7369	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 699	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1548  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  oveq123i  7374  caovdir  7594  caovdilem  7595  caovlem2  7596  cnfcom2  9618  canthwelem  10568  adderpqlem  10872  addassnq  10876  distrnq  10879  ltanq  10889  1lt2nq  10891  ltexnq  10893  halfnq  10894  mulcmpblnrlem  10988  mulcomsr  11007  distrsr  11009  m1p1sr  11010  m1m1sr  11011  mulgt0sr  11023  addcnsrec  11061  mulcnsrec  11062  axmulcom  11073  axmulass  11075  axdistr  11076  axi2m1  11077  addrid  11321  3t3e9  12338  8th4div3  12392  halfthird  12393  numma  12683  decmul10add  12708  4t3lem  12736  9t11e99  12769  5recm6rec  12782  fz0to3un2pr  13578  seqfeq4  14008  seqof  14016  sqdivi  14142  sq4e2t8  14156  i4  14161  binom2i  14169  nn0opthlem1  14225  facp1  14235  fac2  14236  fac3  14237  fac4  14238  faclbnd4lem1  14250  4bc2eq6  14286  ccat2s1len  14581  ccat2s1p2  14588  cats1len  14817  cats2cat  14819  ofs2  14928  cji  15116  01sqrexlem5  15203  fsumadd  15697  fsumsplitf  15699  fsumsplitsnun  15712  0.999...  15841  fprodmul  15920  fproddiv  15921  fprodsplitf  15948  bpoly3  16018  fsumcube  16020  efsep  16072  ef01bndlem  16146  cos2bnd  16150  rpnnen2lem3  16178  3dvds2dec  16297  flodddiv4  16379  sadeq  16436  gcdaddmlem  16488  bezout  16507  nn0expgcd  16528  nn0gcdsq  16717  pythagtriplem16  16796  4sqlem19  16929  dec5nprm  17032  dec2nprm  17033  mod2xnegi  17037  numexp2x  17044  decsplit  17048  karatsuba  17049  2exp5  17051  2exp11  17055  2exp16  17056  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  funcoppc  17837  estrchom  18088  funcestrcsetclem5  18105  yonedalem3b  18240  ecqusaddd  19162  symgressbas  19352  gsum2dlem2  19941  gsumle  20115  opprrng  20320  isrhm  20453  rngqiprnglinlem2  21289  pzriprng1ALT  21475  evlsval  22066  mamudi  22390  mamudir  22391  oftpos  22439  mamutpos  22445  mdetrlin  22589  mdetrlin2  22594  mdetunilem5  22603  cpmadugsumfi  22864  cnmpt2res  23664  ussval  24246  icopnfhmeo  24932  iccpnfhmeo  24934  pcoass  25013  ovolunlem1a  25485  ioombl1lem3  25549  ioombl1lem4  25550  mbfimaopnlem  25644  itgfsum  25816  iblabslem  25817  itgsplit  25825  dveflem  25968  efhalfpi  26457  efipi  26459  sin2pi  26461  ef2pi  26463  sincosq3sgn  26486  sincosq4sgn  26487  sinq34lt0t  26495  sincos4thpi  26499  tan4thpi  26500  tan4thpiOLD  26501  sincos6thpi  26502  sincos3rdpi  26503  pigt3  26504  pige3ALT  26506  cxpcn3  26734  lawcos  26802  1cubrlem  26827  quart1lem  26841  quart1  26842  asin1  26880  atancj  26896  atanlogsublem  26901  log2cnv  26930  log2tlbnd  26931  log2ublem3  26934  log2ub  26935  birthday  26940  basellem8  27073  basellem9  27074  cht2  27157  cht3  27158  1sgm2ppw  27185  bclbnd  27265  bposlem8  27276  bposlem9  27277  lgsdi  27319  lgsquadlem1  27365  2lgsoddprmlem3c  27397  2lgsoddprmlem3d  27398  addsqnreup  27428  addsval2  27977  addsunif  28016  addsasslem1  28017  addsasslem2  28018  negsval  28039  neg0s  28040  neg1s  28041  negsid  28055  mulsval2  28125  muls01  28126  mulsproplem2  28131  mulsproplem3  28132  mulsproplem4  28133  mulsproplem5  28134  mulsproplem6  28135  mulsproplem7  28136  mulsproplem8  28137  mulsproplem12  28141  mulsproplem13  28142  mulsproplem14  28143  mulsunif  28164  addsdilem1  28165  addsdilem2  28166  mulsasslem1  28177  mulsasslem2  28178  mulsunif2  28184  precsexlem11  28231  onmulscl  28292  twocut  28437  mirauto  28774  axsegconlem9  29016  ax5seglem7  29026  vtxdginducedm1  29634  clwlkclwwlkfo  30101  eupth2eucrct  30309  ex-exp  30542  ex-fac  30543  ex-bc  30544  ex-hash  30545  ip0i  30918  ip1ilem  30919  ip2i  30921  ipdirilem  30922  ipasslem10  30932  ip2dii  30937  pythi  30943  siilem1  30944  hvsubsub4i  31152  hvsubcan2i  31157  hisubcomi  31197  normlem0  31202  normlem1  31203  normlem2  31204  normlem3  31205  normlem6  31208  normlem8  31210  normlem9  31211  bcseqi  31213  norm-ii-i  31230  norm-iii-i  31232  normpythi  31235  norm3difi  31240  normpari  31247  normpar2i  31249  polid2i  31250  polidi  31251  bcsiALT  31272  lediri  31630  h1de2i  31646  cmcmlem  31684  cmbr2i  31689  cm2j  31713  fh3i  31716  fh4i  31717  pjaddii  31768  pjsslem  31772  pjssmii  31774  pjdifnormii  31776  lnopeq0lem1  32098  lnopunilem1  32103  lnophmlem2  32110  pjsdi2i  32250  pjclem1  32288  golem1  32364  dpmul100  32979  dpmul1000  32981  dpadd2  32992  dpadd  32993  dpadd3  32994  dpmul  32995  dpmul4  32996  ccatws1f1o  33034  elrgspnlem2  33328  matdim  33811  fldext2chn  33924  constrextdg2lem  33944  constrext2chnlem  33946  iconstr  33962  cos9thpiminplylem4  33981  cos9thpiminplylem5  33982  rmulccn  34124  raddcn  34125  xrmulc1cn  34126  xrge0iifhmeo  34132  qqh0  34180  qqh1  34181  elmbfmvol2  34463  mbfmcnt  34464  eulerpartlemgvv  34572  eulerpartlemgh  34574  fib2  34598  fib3  34599  fib4  34600  fib5  34601  fib6  34602  ballotlem2  34685  ballotlemfval0  34692  ballotth  34734  hgt750lem2  34848  problem2  35909  problem4  35911  quad3  35913  ditgeq123i  36452  cbvditgvw2  36492  poimirlem30  38032  iblabsnclem  38065  dalem10  40180  cdleme0e  40724  cdleme7c  40752  cdleme20c  40818  3exp7  42553  3lexlogpow5ineq1  42554  3lexlogpow5ineq5  42560  aks4d1p1  42576  5bc2eq10  42642  aks5lem3a  42689  sn-1ne2  42763  sqmid3api  42775  sqdeccom12  42781  sq3deccom12  42782  tan3rdpi  42844  sin2t3rdpi  42845  cos2t3rdpi  42846  rei4  42916  ipiiie0  42930  sn-0tie0  42956  mzpcompact2lem  43215  pellexlem5  43293  pellfundgt1  43343  jm2.27c  43467  areaquad  43676  resqrtvalex  44104  imsqrtvalex  44105  lhe4.4ex1a  44788  mccl  46057  dvnprodlem2  46404  itgsin0pilem1  46407  stoweidlem13  46470  wallispilem4  46525  wallispi2lem1  46528  wallispi2lem2  46529  dirkerper  46553  dirkertrigeqlem1  46555  fourierdlem30  46594  fourierdlem47  46610  fourierdlem103  46666  fourierdlem104  46667  fouriersw  46688  etransclem37  46728  sge0splitmpt  46868  sge0xaddlem2  46891  sge0xadd  46892  caragen0  46963  caragenuncllem  46969  nthrucw  47345  goldrasin  47359  goldratmolem2  47363  fsumsplitsndif  47858  139prmALT  48088  127prm  48091  m11nprm  48093  3exp4mod41  48108  ppivalnn4  48119  sbgoldbo  48292  2t6m3t4e0  48853  lincsum  48934  zlmodzxzequa  49001  zlmodzxzequap  49004  zlmodzxzldeplem3  49007  rrx2linest  49247  line2  49257  itsclc0yqsollem1  49267  itsclquadb  49281  itscnhlinecirc02plem2  49288  postcofval  49868  postcofcl  49869  precofval  49871  precofvalALT  49872  precofcl  49874  termcfuncval  50036