Theorem oveq12i 7421

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  oveq123i  7423  caovdir  7644  caovdilem  7645  caovlem2  7646  cnfcom2  9681  canthwelem  10692  adderpqlem  10996  addassnq  11000  distrnq  11003  ltanq  11013  1lt2nq  11015  ltexnq  11017  halfnq  11018  mulcmpblnrlem  11112  mulcomsr  11131  distrsr  11133  m1p1sr  11134  m1m1sr  11135  mulgt0sr  11147  addcnsrec  11185  mulcnsrec  11186  axmulcom  11197  axmulass  11199  axdistr  11200  axi2m1  11201  addrid  11447  3t3e9  12465  8th4div3  12521  halfthird  12522  numma  12818  decmul10add  12843  4t3lem  12871  9t11e99OLD  12905  5recm6rec  12919  fz0to3un2pr  13717  seqfeq4  14148  seqof  14156  sqdivi  14282  sq4e2t8  14296  i4  14301  binom2i  14309  nn0opthlem1  14365  facp1  14375  fac2  14376  fac3  14377  fac4  14378  faclbnd4lem1  14390  4bc2eq6  14426  ccat2s1len  14724  ccat2s1p2  14731  cats1len  14964  cats2cat  14966  ofs2  15077  cji  15279  01sqrexlem5  15366  fsumadd  15859  fsumsplitf  15861  fsumsplitsnun  15874  0.999...  16003  fprodmul  16080  fproddiv  16081  fprodsplitf  16108  bpoly3  16177  fsumcube  16179  efsep  16231  ef01bndlem  16305  cos2bnd  16309  rpnnen2lem3  16337  3dvds2dec  16456  flodddiv4  16538  sadeq  16595  gcdaddmlem  16647  bezout  16666  nn0expgcd  16687  nn0gcdsq  16876  pythagtriplem16  16955  4sqlem19  17088  dec5nprm  17191  dec2nprm  17192  mod2xnegi  17196  numexp2x  17203  decsplit  17207  karatsuba  17208  2exp5  17210  2exp11  17214  2exp16  17215  37prm  17246  43prm  17247  83prm  17248  139prm  17249  163prm  17250  317prm  17251  631prm  17252  1259lem1  17256  1259lem2  17257  1259lem3  17258  1259lem4  17259  1259lem5  17260  1259prm  17261  2503lem1  17262  2503lem2  17263  2503lem3  17264  2503prm  17265  4001lem1  17266  4001lem2  17267  4001lem3  17268  4001lem4  17269  4001prm  17270  funcoppc  17997  estrchom  18248  funcestrcsetclem5  18265  yonedalem3b  18400  ecqusaddd  19354  symgressbas  19543  gsum2dlem2  20132  gsumle  20306  opprrng  20522  isrhm  20656  rngqiprnglinlem2  21535  pzriprng1ALT  21749  evlsval  22342  mamudi  22665  mamudir  22666  oftpos  22714  mamutpos  22720  mdetrlin  22864  mdetrlin2  22869  mdetunilem5  22878  cpmadugsumfi  23142  cnmpt2res  23943  ussval  24525  icopnfhmeo  25211  iccpnfhmeo  25213  pcoass  25292  ovolunlem1a  25764  ioombl1lem3  25828  ioombl1lem4  25829  mbfimaopnlem  25923  itgfsum  26094  iblabslem  26095  itgsplit  26103  dveflem  26246  efhalfpi  26749  efipi  26751  sin2pi  26753  ef2pi  26755  sincosq3sgn  26778  sincosq4sgn  26779  sinq34lt0t  26787  sincos4thpi  26791  tan4thpi  26792  sincos6thpi  26793  sincos3rdpi  26794  pigt3  26795  pige3ALT  26797  cxpcn3  27025  lawcos  27093  1cubrlem  27118  quart1lem  27132  quart1  27133  asin1  27171  atancj  27187  atanlogsublem  27192  log2cnv  27221  log2tlbnd  27222  log2ublem3  27225  log2ub  27226  birthday  27231  basellem8  27364  basellem9  27365  cht2  27448  cht3  27449  1sgm2ppw  27476  bclbnd  27556  bposlem8  27567  bposlem9  27568  lgsdi  27610  lgsquadlem1  27656  2lgsoddprmlem3c  27688  2lgsoddprmlem3d  27689  addsqnreup  27719  addsval2  28268  addsunif  28307  addsasslem1  28308  addsasslem2  28309  negsval  28330  neg0s  28331  neg1s  28332  negsid  28346  mulsval2  28416  muls01  28417  mulsproplem2  28422  mulsproplem3  28423  mulsproplem4  28424  mulsproplem5  28425  mulsproplem6  28426  mulsproplem7  28427  mulsproplem8  28428  mulsproplem12  28432  mulsproplem13  28433  mulsproplem14  28434  mulsunif  28455  addsdilem1  28456  addsdilem2  28457  mulsasslem1  28468  mulsasslem2  28469  mulsunif2  28475  precsexlem11  28522  onmulscl  28583  twocut  28728  mirauto  29075  axsegconlem9  29422  ax5seglem7  29432  vtxdginducedm1  30043  clwlkclwwlkfo  30519  eupth2eucrct  30737  ex-exp  30970  ex-fac  30971  ex-bc  30972  ex-hash  30973  ip0i  31346  ip1ilem  31347  ip2i  31349  ipdirilem  31350  ipasslem10  31360  ip2dii  31365  pythi  31371  siilem1  31372  hvsubsub4i  31580  hvsubcan2i  31585  hisubcomi  31625  normlem0  31630  normlem1  31631  normlem2  31632  normlem3  31633  normlem6  31636  normlem8  31638  normlem9  31639  bcseqi  31641  norm-ii-i  31658  norm-iii-i  31660  normpythi  31663  norm3difi  31668  normpari  31675  normpar2i  31677  polid2i  31678  polidi  31679  bcsiALT  31700  lediri  32058  h1de2i  32074  cmcmlem  32112  cmbr2i  32117  cm2j  32141  fh3i  32144  fh4i  32145  pjaddii  32196  pjsslem  32200  pjssmii  32202  pjdifnormii  32204  lnopeq0lem1  32526  lnopunilem1  32531  lnophmlem2  32538  pjsdi2i  32678  pjclem1  32716  golem1  32792  dpmul100  33382  dpmul1000  33384  dpadd2  33395  dpadd  33396  dpadd3  33397  dpmul  33398  dpmul4  33399  ccatws1f1o  33433  elrgspnlem2  33723  matdim  34166  fldext2chn  34279  constrextdg2lem  34299  constrext2chnlem  34301  iconstr  34317  cos9thpiminplylem4  34336  cos9thpiminplylem5  34337  rmulccn  34479  raddcn  34480  xrmulc1cn  34481  xrge0iifhmeo  34487  qqh0  34535  qqh1  34536  elmbfmvol2  34819  mbfmcnt  34820  eulerpartlemgvv  34928  eulerpartlemgh  34930  fib2  34954  fib3  34955  fib4  34956  fib5  34957  fib6  34958  ballotlem2  35041  ballotlemfval0  35048  ballotth  35090  hgt750lem2  35201  problem2  36346  problem4  36348  quad3  36350  ditgeq123i  36914  cbvditgvw2  36954  poimirlem30  38482  iblabsnclem  38515  dalem10  40644  cdleme0e  41188  cdleme7c  41216  cdleme20c  41282  3exp7  43017  3lexlogpow5ineq1  43018  3lexlogpow5ineq5  43024  aks4d1p1  43040  5bc2eq10  43106  aks5lem3a  43153  25or6to4  43170  sn-1ne2  43244  sqmid3api  43256  sqdeccom12  43262  sq3deccom12  43263  tan3rdpi  43325  sin2t3rdpi  43326  cos2t3rdpi  43327  rei4  43397  ipiiie0  43411  sn-0tie0  43437  mzpcompact2lem  43694  pellexlem5  43772  pellfundgt1  43822  jm2.27c  43946  areaquad  44155  resqrtvalex  44583  imsqrtvalex  44584  lhe4.4ex1a  45251  mccl  46526  dvnprodlem2  46873  itgsin0pilem1  46876  stoweidlem13  46939  wallispilem4  46994  wallispi2lem1  46997  wallispi2lem2  46998  dirkerper  47022  dirkertrigeqlem1  47024  fourierdlem30  47063  fourierdlem47  47079  fourierdlem103  47135  fourierdlem104  47136  fouriersw  47157  etransclem37  47197  sge0splitmpt  47337  sge0xaddlem2  47360  sge0xadd  47361  caragen0  47432  caragenuncllem  47438  goldpolyfactor  47843  goldrasin  47845  goldratmolem2  47849  goldratmolem3  47850  goldratval  47852  fsumsplitsndif  48367  139prmALT  48597  127prm  48600  m11nprm  48602  3exp4mod41  48617  ppivalnn4  48628  sbgoldbo  48801  2t6m3t4e0  49376  lincsum  49457  zlmodzxzequa  49524  zlmodzxzequap  49527  zlmodzxzldeplem3  49530  rrx2linest  49770  line2  49780  itsclc0yqsollem1  49790  itsclquadb  49804  itscnhlinecirc02plem2  49811  postcofval  50388  postcofcl  50389  precofval  50391  precofvalALT  50392  precofcl  50394  termcfuncval  50556