Theorem oveq12i 7399

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

Syntax hints:   = wceq 1540  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  oveq123i  7401  caovdir  7623  caovdilem  7624  caovlem2  7625  cnfcom2  9655  canthwelem  10603  adderpqlem  10907  addassnq  10911  distrnq  10914  ltanq  10924  1lt2nq  10926  ltexnq  10928  halfnq  10929  mulcmpblnrlem  11023  mulcomsr  11042  distrsr  11044  m1p1sr  11045  m1m1sr  11046  mulgt0sr  11058  addcnsrec  11096  mulcnsrec  11097  axmulcom  11108  axmulass  11110  axdistr  11111  axi2m1  11112  addrid  11354  3t3e9  12348  8th4div3  12402  halfthird  12403  numma  12693  decmul10add  12718  4t3lem  12746  9t11e99  12779  5recm6rec  12792  fz0to3un2pr  13590  seqfeq4  14016  seqof  14024  sqdivi  14150  sq4e2t8  14164  i4  14169  binom2i  14177  nn0opthlem1  14233  facp1  14243  fac2  14244  fac3  14245  fac4  14246  faclbnd4lem1  14258  4bc2eq6  14294  ccat2s1len  14588  ccat2s1p2  14595  cats1len  14826  cats2cat  14828  ofs2  14937  cji  15125  01sqrexlem5  15212  fsumadd  15706  fsumsplitf  15708  fsumsplitsnun  15721  0.999...  15847  fprodmul  15926  fproddiv  15927  fprodsplitf  15954  bpoly3  16024  fsumcube  16026  efsep  16078  ef01bndlem  16152  cos2bnd  16156  rpnnen2lem3  16184  3dvds2dec  16303  flodddiv4  16385  sadeq  16442  gcdaddmlem  16494  bezout  16513  nn0expgcd  16534  nn0gcdsq  16722  pythagtriplem16  16801  4sqlem19  16934  dec5nprm  17037  dec2nprm  17038  mod2xnegi  17042  numexp2x  17049  decsplit  17053  karatsuba  17054  2exp5  17056  2exp11  17060  2exp16  17061  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  funcoppc  17837  estrchom  18088  funcestrcsetclem5  18105  yonedalem3b  18240  ecqusaddd  19124  symgressbas  19312  gsum2dlem2  19901  opprrng  20254  isrhm  20387  rngqiprnglinlem2  21202  pzriprng1ALT  21406  evlsval  21993  mamudi  22290  mamudir  22291  oftpos  22339  mamutpos  22345  mdetrlin  22489  mdetrlin2  22494  mdetunilem5  22503  cpmadugsumfi  22764  cnmpt2res  23564  ussval  24147  icopnfhmeo  24841  iccpnfhmeo  24843  pcoass  24924  ovolunlem1a  25397  ioombl1lem3  25461  ioombl1lem4  25462  mbfimaopnlem  25556  itgfsum  25728  iblabslem  25729  itgsplit  25737  dveflem  25883  efhalfpi  26380  efipi  26382  sin2pi  26384  ef2pi  26386  sincosq3sgn  26409  sincosq4sgn  26410  sinq34lt0t  26418  sincos4thpi  26422  tan4thpi  26423  tan4thpiOLD  26424  sincos6thpi  26425  sincos3rdpi  26426  pigt3  26427  pige3ALT  26429  cxpcn3  26658  lawcos  26726  1cubrlem  26751  quart1lem  26765  quart1  26766  asin1  26804  atancj  26820  atanlogsublem  26825  log2cnv  26854  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  birthday  26864  basellem8  26998  basellem9  26999  cht2  27082  cht3  27083  1sgm2ppw  27111  bclbnd  27191  bposlem8  27202  bposlem9  27203  lgsdi  27245  lgsquadlem1  27291  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  addsqnreup  27354  addsval2  27870  addsunif  27909  addsasslem1  27910  addsasslem2  27911  negsval  27931  negs0s  27932  negs1s  27933  negsid  27947  mulsval2  28014  muls01  28015  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsunif  28053  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  mulsunif2  28073  precsexlem11  28119  onmulscl  28175  1p1e2s  28302  twocut  28309  0reno  28348  mirauto  28611  axsegconlem9  28852  ax5seglem7  28862  vtxdginducedm1  29471  clwlkclwwlkfo  29938  eupth2eucrct  30146  ex-exp  30379  ex-fac  30380  ex-bc  30381  ex-hash  30382  ip0i  30754  ip1ilem  30755  ip2i  30757  ipdirilem  30758  ipasslem10  30768  ip2dii  30773  pythi  30779  siilem1  30780  hvsubsub4i  30988  hvsubcan2i  30993  hisubcomi  31033  normlem0  31038  normlem1  31039  normlem2  31040  normlem3  31041  normlem6  31044  normlem8  31046  normlem9  31047  bcseqi  31049  norm-ii-i  31066  norm-iii-i  31068  normpythi  31071  norm3difi  31076  normpari  31083  normpar2i  31085  polid2i  31086  polidi  31087  bcsiALT  31108  lediri  31466  h1de2i  31482  cmcmlem  31520  cmbr2i  31525  cm2j  31549  fh3i  31552  fh4i  31553  pjaddii  31604  pjsslem  31608  pjssmii  31610  pjdifnormii  31612  lnopeq0lem1  31934  lnopunilem1  31939  lnophmlem2  31946  pjsdi2i  32086  pjclem1  32124  golem1  32200  dpmul100  32817  dpmul1000  32819  dpadd2  32830  dpadd  32831  dpadd3  32832  dpmul  32833  dpmul4  32834  ccatws1f1o  32873  gsumle  33038  elrgspnlem2  33194  matdim  33611  fldext2chn  33718  constrextdg2lem  33738  constrext2chnlem  33740  iconstr  33756  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  rmulccn  33918  raddcn  33919  xrmulc1cn  33920  xrge0iifhmeo  33926  qqh0  33974  qqh1  33975  elmbfmvol2  34258  mbfmcnt  34259  eulerpartlemgvv  34367  eulerpartlemgh  34369  fib2  34393  fib3  34394  fib4  34395  fib5  34396  fib6  34397  ballotlem2  34480  ballotlemfval0  34487  ballotth  34529  hgt750lem2  34643  problem2  35653  problem4  35655  quad3  35657  ditgeq123i  36197  cbvditgvw2  36237  poimirlem30  37644  iblabsnclem  37677  dalem10  39667  cdleme0e  40211  cdleme7c  40239  cdleme20c  40305  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  5bc2eq10  42130  aks5lem3a  42177  sn-1ne2  42253  sqmid3api  42271  sqdeccom12  42277  sq3deccom12  42278  tan3rdpi  42340  sin2t3rdpi  42341  cos2t3rdpi  42342  rei4  42412  ipiiie0  42426  sn-0tie0  42439  mzpcompact2lem  42739  pellexlem5  42821  pellfundgt1  42871  jm2.27c  42996  areaquad  43205  resqrtvalex  43634  imsqrtvalex  43635  lhe4.4ex1a  44318  mccl  45596  dvnprodlem2  45945  itgsin0pilem1  45948  stoweidlem13  46011  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  dirkerper  46094  dirkertrigeqlem1  46096  fourierdlem30  46135  fourierdlem47  46151  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  etransclem37  46269  sge0splitmpt  46409  sge0xaddlem2  46432  sge0xadd  46433  caragen0  46504  caragenuncllem  46510  fsumsplitsndif  47374  139prmALT  47597  127prm  47600  m11nprm  47602  3exp4mod41  47617  sbgoldbo  47788  2t6m3t4e0  48336  lincsum  48418  zlmodzxzequa  48485  zlmodzxzequap  48488  zlmodzxzldeplem3  48491  rrx2linest  48731  line2  48741  itsclc0yqsollem1  48751  itsclquadb  48765  itscnhlinecirc02plem2  48772  postcofval  49353  postcofcl  49354  precofval  49356  precofvalALT  49357  precofcl  49359  termcfuncval  49521