Theorem oveq12i 7402

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  oveq123i  7404  caovdir  7626  caovdilem  7627  caovlem2  7628  cnfcom2  9662  canthwelem  10610  adderpqlem  10914  addassnq  10918  distrnq  10921  ltanq  10931  1lt2nq  10933  ltexnq  10935  halfnq  10936  mulcmpblnrlem  11030  mulcomsr  11049  distrsr  11051  m1p1sr  11052  m1m1sr  11053  mulgt0sr  11065  addcnsrec  11103  mulcnsrec  11104  axmulcom  11115  axmulass  11117  axdistr  11118  axi2m1  11119  addrid  11361  3t3e9  12355  8th4div3  12409  halfthird  12410  numma  12700  decmul10add  12725  4t3lem  12753  9t11e99  12786  5recm6rec  12799  fz0to3un2pr  13597  seqfeq4  14023  seqof  14031  sqdivi  14157  sq4e2t8  14171  i4  14176  binom2i  14184  nn0opthlem1  14240  facp1  14250  fac2  14251  fac3  14252  fac4  14253  faclbnd4lem1  14265  4bc2eq6  14301  ccat2s1len  14595  ccat2s1p2  14602  cats1len  14833  cats2cat  14835  ofs2  14944  cji  15132  01sqrexlem5  15219  fsumadd  15713  fsumsplitf  15715  fsumsplitsnun  15728  0.999...  15854  fprodmul  15933  fproddiv  15934  fprodsplitf  15961  bpoly3  16031  fsumcube  16033  efsep  16085  ef01bndlem  16159  cos2bnd  16163  rpnnen2lem3  16191  3dvds2dec  16310  flodddiv4  16392  sadeq  16449  gcdaddmlem  16501  bezout  16520  nn0expgcd  16541  nn0gcdsq  16729  pythagtriplem16  16808  4sqlem19  16941  dec5nprm  17044  dec2nprm  17045  mod2xnegi  17049  numexp2x  17056  decsplit  17060  karatsuba  17061  2exp5  17063  2exp11  17067  2exp16  17068  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  funcoppc  17844  estrchom  18095  funcestrcsetclem5  18112  yonedalem3b  18247  ecqusaddd  19131  symgressbas  19319  gsum2dlem2  19908  opprrng  20261  isrhm  20394  rngqiprnglinlem2  21209  pzriprng1ALT  21413  evlsval  22000  mamudi  22297  mamudir  22298  oftpos  22346  mamutpos  22352  mdetrlin  22496  mdetrlin2  22501  mdetunilem5  22510  cpmadugsumfi  22771  cnmpt2res  23571  ussval  24154  icopnfhmeo  24848  iccpnfhmeo  24850  pcoass  24931  ovolunlem1a  25404  ioombl1lem3  25468  ioombl1lem4  25469  mbfimaopnlem  25563  itgfsum  25735  iblabslem  25736  itgsplit  25744  dveflem  25890  efhalfpi  26387  efipi  26389  sin2pi  26391  ef2pi  26393  sincosq3sgn  26416  sincosq4sgn  26417  sinq34lt0t  26425  sincos4thpi  26429  tan4thpi  26430  tan4thpiOLD  26431  sincos6thpi  26432  sincos3rdpi  26433  pigt3  26434  pige3ALT  26436  cxpcn3  26665  lawcos  26733  1cubrlem  26758  quart1lem  26772  quart1  26773  asin1  26811  atancj  26827  atanlogsublem  26832  log2cnv  26861  log2tlbnd  26862  log2ublem3  26865  log2ub  26866  birthday  26871  basellem8  27005  basellem9  27006  cht2  27089  cht3  27090  1sgm2ppw  27118  bclbnd  27198  bposlem8  27209  bposlem9  27210  lgsdi  27252  lgsquadlem1  27298  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  addsqnreup  27361  addsval2  27877  addsunif  27916  addsasslem1  27917  addsasslem2  27918  negsval  27938  negs0s  27939  negs1s  27940  negsid  27954  mulsval2  28021  muls01  28022  mulsproplem2  28027  mulsproplem3  28028  mulsproplem4  28029  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  mulsunif  28060  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  mulsunif2  28080  precsexlem11  28126  onmulscl  28182  1p1e2s  28309  twocut  28316  0reno  28355  mirauto  28618  axsegconlem9  28859  ax5seglem7  28869  vtxdginducedm1  29478  clwlkclwwlkfo  29945  eupth2eucrct  30153  ex-exp  30386  ex-fac  30387  ex-bc  30388  ex-hash  30389  ip0i  30761  ip1ilem  30762  ip2i  30764  ipdirilem  30765  ipasslem10  30775  ip2dii  30780  pythi  30786  siilem1  30787  hvsubsub4i  30995  hvsubcan2i  31000  hisubcomi  31040  normlem0  31045  normlem1  31046  normlem2  31047  normlem3  31048  normlem6  31051  normlem8  31053  normlem9  31054  bcseqi  31056  norm-ii-i  31073  norm-iii-i  31075  normpythi  31078  norm3difi  31083  normpari  31090  normpar2i  31092  polid2i  31093  polidi  31094  bcsiALT  31115  lediri  31473  h1de2i  31489  cmcmlem  31527  cmbr2i  31532  cm2j  31556  fh3i  31559  fh4i  31560  pjaddii  31611  pjsslem  31615  pjssmii  31617  pjdifnormii  31619  lnopeq0lem1  31941  lnopunilem1  31946  lnophmlem2  31953  pjsdi2i  32093  pjclem1  32131  golem1  32207  dpmul100  32824  dpmul1000  32826  dpadd2  32837  dpadd  32838  dpadd3  32839  dpmul  32840  dpmul4  32841  ccatws1f1o  32880  gsumle  33045  elrgspnlem2  33201  matdim  33618  fldext2chn  33725  constrextdg2lem  33745  constrext2chnlem  33747  iconstr  33763  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  rmulccn  33925  raddcn  33926  xrmulc1cn  33927  xrge0iifhmeo  33933  qqh0  33981  qqh1  33982  elmbfmvol2  34265  mbfmcnt  34266  eulerpartlemgvv  34374  eulerpartlemgh  34376  fib2  34400  fib3  34401  fib4  34402  fib5  34403  fib6  34404  ballotlem2  34487  ballotlemfval0  34494  ballotth  34536  hgt750lem2  34650  problem2  35660  problem4  35662  quad3  35664  ditgeq123i  36204  cbvditgvw2  36244  poimirlem30  37651  iblabsnclem  37684  dalem10  39674  cdleme0e  40218  cdleme7c  40246  cdleme20c  40312  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1  42071  5bc2eq10  42137  aks5lem3a  42184  sn-1ne2  42260  sqmid3api  42278  sqdeccom12  42284  sq3deccom12  42285  tan3rdpi  42347  sin2t3rdpi  42348  cos2t3rdpi  42349  rei4  42419  ipiiie0  42433  sn-0tie0  42446  mzpcompact2lem  42746  pellexlem5  42828  pellfundgt1  42878  jm2.27c  43003  areaquad  43212  resqrtvalex  43641  imsqrtvalex  43642  lhe4.4ex1a  44325  mccl  45603  dvnprodlem2  45952  itgsin0pilem1  45955  stoweidlem13  46018  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  dirkerper  46101  dirkertrigeqlem1  46103  fourierdlem30  46142  fourierdlem47  46158  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  etransclem37  46276  sge0splitmpt  46416  sge0xaddlem2  46439  sge0xadd  46440  caragen0  46511  caragenuncllem  46517  fsumsplitsndif  47378  139prmALT  47601  127prm  47604  m11nprm  47606  3exp4mod41  47621  sbgoldbo  47792  2t6m3t4e0  48340  lincsum  48422  zlmodzxzequa  48489  zlmodzxzequap  48492  zlmodzxzldeplem3  48495  rrx2linest  48735  line2  48745  itsclc0yqsollem1  48755  itsclquadb  48769  itscnhlinecirc02plem2  48776  postcofval  49357  postcofcl  49358  precofval  49360  precofvalALT  49361  precofcl  49363  termcfuncval  49525