Theorem oveq12i 7368

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

Syntax hints:   = wceq 1541  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  oveq123i  7370  caovdir  7590  caovdilem  7591  caovlem2  7592  cnfcom2  9609  canthwelem  10559  adderpqlem  10863  addassnq  10867  distrnq  10870  ltanq  10880  1lt2nq  10882  ltexnq  10884  halfnq  10885  mulcmpblnrlem  10979  mulcomsr  10998  distrsr  11000  m1p1sr  11001  m1m1sr  11002  mulgt0sr  11014  addcnsrec  11052  mulcnsrec  11053  axmulcom  11064  axmulass  11066  axdistr  11067  axi2m1  11068  addrid  11311  3t3e9  12305  8th4div3  12359  halfthird  12360  numma  12649  decmul10add  12674  4t3lem  12702  9t11e99  12735  5recm6rec  12748  fz0to3un2pr  13543  seqfeq4  13972  seqof  13980  sqdivi  14106  sq4e2t8  14120  i4  14125  binom2i  14133  nn0opthlem1  14189  facp1  14199  fac2  14200  fac3  14201  fac4  14202  faclbnd4lem1  14214  4bc2eq6  14250  ccat2s1len  14545  ccat2s1p2  14552  cats1len  14781  cats2cat  14783  ofs2  14892  cji  15080  01sqrexlem5  15167  fsumadd  15661  fsumsplitf  15663  fsumsplitsnun  15676  0.999...  15802  fprodmul  15881  fproddiv  15882  fprodsplitf  15909  bpoly3  15979  fsumcube  15981  efsep  16033  ef01bndlem  16107  cos2bnd  16111  rpnnen2lem3  16139  3dvds2dec  16258  flodddiv4  16340  sadeq  16397  gcdaddmlem  16449  bezout  16468  nn0expgcd  16489  nn0gcdsq  16677  pythagtriplem16  16756  4sqlem19  16889  dec5nprm  16992  dec2nprm  16993  mod2xnegi  16997  numexp2x  17004  decsplit  17008  karatsuba  17009  2exp5  17011  2exp11  17015  2exp16  17016  37prm  17046  43prm  17047  83prm  17048  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  funcoppc  17797  estrchom  18048  funcestrcsetclem5  18065  yonedalem3b  18200  ecqusaddd  19119  symgressbas  19309  gsum2dlem2  19898  gsumle  20072  opprrng  20279  isrhm  20412  rngqiprnglinlem2  21245  pzriprng1ALT  21449  evlsval  22039  mamudi  22345  mamudir  22346  oftpos  22394  mamutpos  22400  mdetrlin  22544  mdetrlin2  22549  mdetunilem5  22558  cpmadugsumfi  22819  cnmpt2res  23619  ussval  24201  icopnfhmeo  24895  iccpnfhmeo  24897  pcoass  24978  ovolunlem1a  25451  ioombl1lem3  25515  ioombl1lem4  25516  mbfimaopnlem  25610  itgfsum  25782  iblabslem  25783  itgsplit  25791  dveflem  25937  efhalfpi  26434  efipi  26436  sin2pi  26438  ef2pi  26440  sincosq3sgn  26463  sincosq4sgn  26464  sinq34lt0t  26472  sincos4thpi  26476  tan4thpi  26477  tan4thpiOLD  26478  sincos6thpi  26479  sincos3rdpi  26480  pigt3  26481  pige3ALT  26483  cxpcn3  26712  lawcos  26780  1cubrlem  26805  quart1lem  26819  quart1  26820  asin1  26858  atancj  26874  atanlogsublem  26879  log2cnv  26908  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  birthday  26918  basellem8  27052  basellem9  27053  cht2  27136  cht3  27137  1sgm2ppw  27165  bclbnd  27245  bposlem8  27256  bposlem9  27257  lgsdi  27299  lgsquadlem1  27345  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  addsqnreup  27408  addsval2  27933  addsunif  27972  addsasslem1  27973  addsasslem2  27974  negsval  27994  negs0s  27995  negs1s  27996  negsid  28010  mulsval2  28080  muls01  28081  mulsproplem2  28086  mulsproplem3  28087  mulsproplem4  28088  mulsproplem5  28089  mulsproplem6  28090  mulsproplem7  28091  mulsproplem8  28092  mulsproplem12  28096  mulsproplem13  28097  mulsproplem14  28098  mulsunif  28119  addsdilem1  28120  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  mulsunif2  28139  precsexlem11  28185  onmulscl  28242  1p1e2s  28374  twocut  28381  mirauto  28705  axsegconlem9  28947  ax5seglem7  28957  vtxdginducedm1  29566  clwlkclwwlkfo  30033  eupth2eucrct  30241  ex-exp  30474  ex-fac  30475  ex-bc  30476  ex-hash  30477  ip0i  30849  ip1ilem  30850  ip2i  30852  ipdirilem  30853  ipasslem10  30863  ip2dii  30868  pythi  30874  siilem1  30875  hvsubsub4i  31083  hvsubcan2i  31088  hisubcomi  31128  normlem0  31133  normlem1  31134  normlem2  31135  normlem3  31136  normlem6  31139  normlem8  31141  normlem9  31142  bcseqi  31144  norm-ii-i  31161  norm-iii-i  31163  normpythi  31166  norm3difi  31171  normpari  31178  normpar2i  31180  polid2i  31181  polidi  31182  bcsiALT  31203  lediri  31561  h1de2i  31577  cmcmlem  31615  cmbr2i  31620  cm2j  31644  fh3i  31647  fh4i  31648  pjaddii  31699  pjsslem  31703  pjssmii  31705  pjdifnormii  31707  lnopeq0lem1  32029  lnopunilem1  32034  lnophmlem2  32041  pjsdi2i  32181  pjclem1  32219  golem1  32295  dpmul100  32927  dpmul1000  32929  dpadd2  32940  dpadd  32941  dpadd3  32942  dpmul  32943  dpmul4  32944  ccatws1f1o  32982  elrgspnlem2  33274  matdim  33721  fldext2chn  33834  constrextdg2lem  33854  constrext2chnlem  33856  iconstr  33872  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  rmulccn  34034  raddcn  34035  xrmulc1cn  34036  xrge0iifhmeo  34042  qqh0  34090  qqh1  34091  elmbfmvol2  34373  mbfmcnt  34374  eulerpartlemgvv  34482  eulerpartlemgh  34484  fib2  34508  fib3  34509  fib4  34510  fib5  34511  fib6  34512  ballotlem2  34595  ballotlemfval0  34602  ballotth  34644  hgt750lem2  34758  problem2  35809  problem4  35811  quad3  35813  ditgeq123i  36352  cbvditgvw2  36392  poimirlem30  37790  iblabsnclem  37823  dalem10  39872  cdleme0e  40416  cdleme7c  40444  cdleme20c  40510  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1  42269  5bc2eq10  42335  aks5lem3a  42382  sn-1ne2  42462  sqmid3api  42480  sqdeccom12  42486  sq3deccom12  42487  tan3rdpi  42549  sin2t3rdpi  42550  cos2t3rdpi  42551  rei4  42621  ipiiie0  42635  sn-0tie0  42648  mzpcompact2lem  42935  pellexlem5  43017  pellfundgt1  43067  jm2.27c  43191  areaquad  43400  resqrtvalex  43828  imsqrtvalex  43829  lhe4.4ex1a  44512  mccl  45786  dvnprodlem2  46133  itgsin0pilem1  46136  stoweidlem13  46199  wallispilem4  46254  wallispi2lem1  46257  wallispi2lem2  46258  dirkerper  46282  dirkertrigeqlem1  46284  fourierdlem30  46323  fourierdlem47  46339  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  etransclem37  46457  sge0splitmpt  46597  sge0xaddlem2  46620  sge0xadd  46621  caragen0  46692  caragenuncllem  46698  nthrucw  47072  fsumsplitsndif  47561  139prmALT  47784  127prm  47787  m11nprm  47789  3exp4mod41  47804  sbgoldbo  47975  2t6m3t4e0  48536  lincsum  48617  zlmodzxzequa  48684  zlmodzxzequap  48687  zlmodzxzldeplem3  48690  rrx2linest  48930  line2  48940  itsclc0yqsollem1  48950  itsclquadb  48964  itscnhlinecirc02plem2  48971  postcofval  49551  postcofcl  49552  precofval  49554  precofvalALT  49555  precofcl  49557  termcfuncval  49719