Theorem oveq12i 7423

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

Syntax hints:   = wceq 1567  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  oveq123i  7425  caovdir  7645  caovdilem  7646  caovlem2  7647  cnfcom2  9671  canthwelem  10635  adderpqlem  10939  addassnq  10943  distrnq  10946  ltanq  10956  1lt2nq  10958  ltexnq  10960  halfnq  10961  mulcmpblnrlem  11055  mulcomsr  11074  distrsr  11076  m1p1sr  11077  m1m1sr  11078  mulgt0sr  11090  addcnsrec  11128  mulcnsrec  11129  axmulcom  11140  axmulass  11142  axdistr  11143  axi2m1  11144  addrid  11390  3t3e9  12408  8th4div3  12464  halfthird  12465  numma  12760  decmul10add  12785  4t3lem  12813  9t11e99OLD  12847  5recm6rec  12861  fz0to3un2pr  13657  seqfeq4  14087  seqof  14095  sqdivi  14221  sq4e2t8  14235  i4  14240  binom2i  14248  nn0opthlem1  14304  facp1  14314  fac2  14315  fac3  14316  fac4  14317  faclbnd4lem1  14329  4bc2eq6  14365  ccat2s1len  14661  ccat2s1p2  14668  cats1len  14897  cats2cat  14899  ofs2  15008  cji  15210  01sqrexlem5  15297  fsumadd  15791  fsumsplitf  15793  fsumsplitsnun  15806  0.999...  15935  fprodmul  16014  fproddiv  16015  fprodsplitf  16042  bpoly3  16112  fsumcube  16114  efsep  16166  ef01bndlem  16240  cos2bnd  16244  rpnnen2lem3  16272  3dvds2dec  16391  flodddiv4  16473  sadeq  16530  gcdaddmlem  16582  bezout  16601  nn0expgcd  16622  nn0gcdsq  16811  pythagtriplem16  16890  4sqlem19  17023  dec5nprm  17126  dec2nprm  17127  mod2xnegi  17131  numexp2x  17138  decsplit  17142  karatsuba  17143  2exp5  17145  2exp11  17149  2exp16  17150  37prm  17181  43prm  17182  83prm  17183  139prm  17184  163prm  17185  317prm  17186  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  1259prm  17196  2503lem1  17197  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem1  17201  4001lem2  17202  4001lem3  17203  4001lem4  17204  4001prm  17205  funcoppc  17932  estrchom  18183  funcestrcsetclem5  18200  yonedalem3b  18335  ecqusaddd  19263  symgressbas  19452  gsum2dlem2  20041  gsumle  20215  opprrng  20427  isrhm  20560  rngqiprnglinlem2  21403  pzriprng1ALT  21615  evlsval  22206  mamudi  22529  mamudir  22530  oftpos  22578  mamutpos  22584  mdetrlin  22728  mdetrlin2  22733  mdetunilem5  22742  cpmadugsumfi  23003  cnmpt2res  23803  ussval  24385  icopnfhmeo  25071  iccpnfhmeo  25073  pcoass  25152  ovolunlem1a  25624  ioombl1lem3  25688  ioombl1lem4  25689  mbfimaopnlem  25783  itgfsum  25955  iblabslem  25956  itgsplit  25964  dveflem  26107  efhalfpi  26602  efipi  26604  sin2pi  26606  ef2pi  26608  sincosq3sgn  26631  sincosq4sgn  26632  sinq34lt0t  26640  sincos4thpi  26644  tan4thpi  26645  tan4thpiOLD  26646  sincos6thpi  26647  sincos3rdpi  26648  pigt3  26649  pige3ALT  26651  cxpcn3  26879  lawcos  26947  1cubrlem  26972  quart1lem  26986  quart1  26987  asin1  27025  atancj  27041  atanlogsublem  27046  log2cnv  27075  log2tlbnd  27076  log2ublem3  27079  log2ub  27080  birthday  27085  basellem8  27218  basellem9  27219  cht2  27302  cht3  27303  1sgm2ppw  27330  bclbnd  27410  bposlem8  27421  bposlem9  27422  lgsdi  27464  lgsquadlem1  27510  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  addsqnreup  27573  addsval2  28122  addsunif  28161  addsasslem1  28162  addsasslem2  28163  negsval  28184  neg0s  28185  neg1s  28186  negsid  28200  mulsval2  28270  muls01  28271  mulsproplem2  28276  mulsproplem3  28277  mulsproplem4  28278  mulsproplem5  28279  mulsproplem6  28280  mulsproplem7  28281  mulsproplem8  28282  mulsproplem12  28286  mulsproplem13  28287  mulsproplem14  28288  mulsunif  28309  addsdilem1  28310  addsdilem2  28311  mulsasslem1  28322  mulsasslem2  28323  mulsunif2  28329  precsexlem11  28376  onmulscl  28437  twocut  28582  mirauto  28923  axsegconlem9  29216  ax5seglem7  29226  vtxdginducedm1  29834  clwlkclwwlkfo  30301  eupth2eucrct  30509  ex-exp  30742  ex-fac  30743  ex-bc  30744  ex-hash  30745  ip0i  31118  ip1ilem  31119  ip2i  31121  ipdirilem  31122  ipasslem10  31132  ip2dii  31137  pythi  31143  siilem1  31144  hvsubsub4i  31352  hvsubcan2i  31357  hisubcomi  31397  normlem0  31402  normlem1  31403  normlem2  31404  normlem3  31405  normlem6  31408  normlem8  31410  normlem9  31411  bcseqi  31413  norm-ii-i  31430  norm-iii-i  31432  normpythi  31435  norm3difi  31440  normpari  31447  normpar2i  31449  polid2i  31450  polidi  31451  bcsiALT  31472  lediri  31830  h1de2i  31846  cmcmlem  31884  cmbr2i  31889  cm2j  31913  fh3i  31916  fh4i  31917  pjaddii  31968  pjsslem  31972  pjssmii  31974  pjdifnormii  31976  lnopeq0lem1  32298  lnopunilem1  32303  lnophmlem2  32310  pjsdi2i  32450  pjclem1  32488  golem1  32564  dpmul100  33157  dpmul1000  33159  dpadd2  33170  dpadd  33171  dpadd3  33172  dpmul  33173  dpmul4  33174  ccatws1f1o  33212  elrgspnlem2  33504  matdim  33950  fldext2chn  34063  constrextdg2lem  34083  constrext2chnlem  34085  iconstr  34101  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  rmulccn  34263  raddcn  34264  xrmulc1cn  34265  xrge0iifhmeo  34271  qqh0  34319  qqh1  34320  elmbfmvol2  34602  mbfmcnt  34603  eulerpartlemgvv  34711  eulerpartlemgh  34713  fib2  34737  fib3  34738  fib4  34739  fib5  34740  fib6  34741  ballotlem2  34824  ballotlemfval0  34831  ballotth  34873  hgt750lem2  34984  problem2  36091  problem4  36093  quad3  36095  ditgeq123i  36644  cbvditgvw2  36684  poimirlem30  38223  iblabsnclem  38256  dalem10  40371  cdleme0e  40915  cdleme7c  40943  cdleme20c  41009  3exp7  42744  3lexlogpow5ineq1  42745  3lexlogpow5ineq5  42751  aks4d1p1  42767  5bc2eq10  42833  aks5lem3a  42880  25or6to4  42897  sn-1ne2  42956  sqmid3api  42968  sqdeccom12  42974  sq3deccom12  42975  tan3rdpi  43037  sin2t3rdpi  43038  cos2t3rdpi  43039  rei4  43109  ipiiie0  43123  sn-0tie0  43149  mzpcompact2lem  43408  pellexlem5  43486  pellfundgt1  43536  jm2.27c  43660  areaquad  43869  resqrtvalex  44297  imsqrtvalex  44298  lhe4.4ex1a  44965  mccl  46240  dvnprodlem2  46587  itgsin0pilem1  46590  stoweidlem13  46653  wallispilem4  46708  wallispi2lem1  46711  wallispi2lem2  46712  dirkerper  46736  dirkertrigeqlem1  46738  fourierdlem30  46777  fourierdlem47  46793  fourierdlem103  46849  fourierdlem104  46850  fouriersw  46871  etransclem37  46911  sge0splitmpt  47051  sge0xaddlem2  47074  sge0xadd  47075  caragen0  47146  caragenuncllem  47152  nthrucw  47528  goldrasin  47542  goldratmolem2  47546  fsumsplitsndif  48041  139prmALT  48271  127prm  48274  m11nprm  48276  3exp4mod41  48291  ppivalnn4  48302  sbgoldbo  48475  2t6m3t4e0  49047  lincsum  49128  zlmodzxzequa  49195  zlmodzxzequap  49198  zlmodzxzldeplem3  49201  rrx2linest  49441  line2  49451  itsclc0yqsollem1  49461  itsclquadb  49475  itscnhlinecirc02plem2  49482  postcofval  50061  postcofcl  50062  precofval  50064  precofvalALT  50065  precofcl  50067  termcfuncval  50229