Theorem oveq12i 7415

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  oveq123i  7417  caovdir  7639  caovdilem  7640  caovlem2  7641  cnfcom2  9714  canthwelem  10662  adderpqlem  10966  addassnq  10970  distrnq  10973  ltanq  10983  1lt2nq  10985  ltexnq  10987  halfnq  10988  mulcmpblnrlem  11082  mulcomsr  11101  distrsr  11103  m1p1sr  11104  m1m1sr  11105  mulgt0sr  11117  addcnsrec  11155  mulcnsrec  11156  axmulcom  11167  axmulass  11169  axdistr  11170  axi2m1  11171  addrid  11413  3t3e9  12405  8th4div3  12459  halfthird  12460  numma  12750  decmul10add  12775  4t3lem  12803  9t11e99  12836  5recm6rec  12849  fz0to3un2pr  13644  seqfeq4  14067  seqof  14075  sqdivi  14201  sq4e2t8  14215  i4  14220  binom2i  14228  nn0opthlem1  14284  facp1  14294  fac2  14295  fac3  14296  fac4  14297  faclbnd4lem1  14309  4bc2eq6  14345  ccat2s1len  14639  ccat2s1p2  14646  cats1len  14877  cats2cat  14879  ofs2  14988  cji  15176  01sqrexlem5  15263  fsumadd  15754  fsumsplitf  15756  fsumsplitsnun  15769  0.999...  15895  fprodmul  15974  fproddiv  15975  fprodsplitf  16002  bpoly3  16072  fsumcube  16074  efsep  16126  ef01bndlem  16200  cos2bnd  16204  rpnnen2lem3  16232  3dvds2dec  16350  flodddiv4  16432  sadeq  16489  gcdaddmlem  16541  bezout  16560  nn0expgcd  16581  nn0gcdsq  16769  pythagtriplem16  16848  4sqlem19  16981  dec5nprm  17084  dec2nprm  17085  mod2xnegi  17089  numexp2x  17096  decsplit  17100  karatsuba  17101  2exp5  17103  2exp11  17107  2exp16  17108  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  funcoppc  17886  estrchom  18137  funcestrcsetclem5  18154  yonedalem3b  18289  ecqusaddd  19173  symgressbas  19361  gsum2dlem2  19950  opprrng  20303  isrhm  20436  rngqiprnglinlem2  21251  pzriprng1ALT  21455  evlsval  22042  mamudi  22339  mamudir  22340  oftpos  22388  mamutpos  22394  mdetrlin  22538  mdetrlin2  22543  mdetunilem5  22552  cpmadugsumfi  22813  cnmpt2res  23613  ussval  24196  icopnfhmeo  24890  iccpnfhmeo  24892  pcoass  24973  ovolunlem1a  25447  ioombl1lem3  25511  ioombl1lem4  25512  mbfimaopnlem  25606  itgfsum  25778  iblabslem  25779  itgsplit  25787  dveflem  25933  efhalfpi  26430  efipi  26432  sin2pi  26434  ef2pi  26436  sincosq3sgn  26459  sincosq4sgn  26460  sinq34lt0t  26468  sincos4thpi  26472  tan4thpi  26473  tan4thpiOLD  26474  sincos6thpi  26475  sincos3rdpi  26476  pigt3  26477  pige3ALT  26479  cxpcn3  26708  lawcos  26776  1cubrlem  26801  quart1lem  26815  quart1  26816  asin1  26854  atancj  26870  atanlogsublem  26875  log2cnv  26904  log2tlbnd  26905  log2ublem3  26908  log2ub  26909  birthday  26914  basellem8  27048  basellem9  27049  cht2  27132  cht3  27133  1sgm2ppw  27161  bclbnd  27241  bposlem8  27252  bposlem9  27253  lgsdi  27295  lgsquadlem1  27341  2lgsoddprmlem3c  27373  2lgsoddprmlem3d  27374  addsqnreup  27404  addsval2  27913  addsunif  27952  addsasslem1  27953  addsasslem2  27954  negsval  27974  negs0s  27975  negs1s  27976  negsid  27990  mulsval2  28054  muls01  28055  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  mulsunif  28093  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  mulsunif2  28113  precsexlem11  28158  onmulscl  28204  1p1e2s  28317  nohalf  28324  0reno  28346  mirauto  28609  axsegconlem9  28850  ax5seglem7  28860  vtxdginducedm1  29469  clwlkclwwlkfo  29936  eupth2eucrct  30144  ex-exp  30377  ex-fac  30378  ex-bc  30379  ex-hash  30380  ip0i  30752  ip1ilem  30753  ip2i  30755  ipdirilem  30756  ipasslem10  30766  ip2dii  30771  pythi  30777  siilem1  30778  hvsubsub4i  30986  hvsubcan2i  30991  hisubcomi  31031  normlem0  31036  normlem1  31037  normlem2  31038  normlem3  31039  normlem6  31042  normlem8  31044  normlem9  31045  bcseqi  31047  norm-ii-i  31064  norm-iii-i  31066  normpythi  31069  norm3difi  31074  normpari  31081  normpar2i  31083  polid2i  31084  polidi  31085  bcsiALT  31106  lediri  31464  h1de2i  31480  cmcmlem  31518  cmbr2i  31523  cm2j  31547  fh3i  31550  fh4i  31551  pjaddii  31602  pjsslem  31606  pjssmii  31608  pjdifnormii  31610  lnopeq0lem1  31932  lnopunilem1  31937  lnophmlem2  31944  pjsdi2i  32084  pjclem1  32122  golem1  32198  dpmul100  32817  dpmul1000  32819  dpadd2  32830  dpadd  32831  dpadd3  32832  dpmul  32833  dpmul4  32834  ccatws1f1o  32873  gsumle  33038  elrgspnlem2  33184  matdim  33601  fldext2chn  33708  constrextdg2lem  33728  constrext2chnlem  33730  iconstr  33746  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  rmulccn  33905  raddcn  33906  xrmulc1cn  33907  xrge0iifhmeo  33913  qqh0  33961  qqh1  33962  elmbfmvol2  34245  mbfmcnt  34246  eulerpartlemgvv  34354  eulerpartlemgh  34356  fib2  34380  fib3  34381  fib4  34382  fib5  34383  fib6  34384  ballotlem2  34467  ballotlemfval0  34474  ballotth  34516  hgt750lem2  34630  problem2  35634  problem4  35636  quad3  35638  ditgeq123i  36173  cbvditgvw2  36213  poimirlem30  37620  iblabsnclem  37653  dalem10  39638  cdleme0e  40182  cdleme7c  40210  cdleme20c  40276  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  aks4d1p1  42035  5bc2eq10  42101  aks5lem3a  42148  sn-1ne2  42262  sqmid3api  42280  sqdeccom12  42286  sq3deccom12  42287  tan3rdpi  42346  rei4  42413  ipiiie0  42427  sn-0tie0  42429  mzpcompact2lem  42721  pellexlem5  42803  pellfundgt1  42853  jm2.27c  42978  areaquad  43187  resqrtvalex  43616  imsqrtvalex  43617  lhe4.4ex1a  44301  mccl  45575  dvnprodlem2  45924  itgsin0pilem1  45927  stoweidlem13  45990  wallispilem4  46045  wallispi2lem1  46048  wallispi2lem2  46049  dirkerper  46073  dirkertrigeqlem1  46075  fourierdlem30  46114  fourierdlem47  46130  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  etransclem37  46248  sge0splitmpt  46388  sge0xaddlem2  46411  sge0xadd  46412  caragen0  46483  caragenuncllem  46489  fsumsplitsndif  47335  139prmALT  47558  127prm  47561  m11nprm  47563  3exp4mod41  47578  sbgoldbo  47749  2t6m3t4e0  48271  lincsum  48353  zlmodzxzequa  48420  zlmodzxzequap  48423  zlmodzxzldeplem3  48426  rrx2linest  48670  line2  48680  itsclc0yqsollem1  48690  itsclquadb  48704  itscnhlinecirc02plem2  48711  postcofval  49223  postcofcl  49224  precofval  49226  precofvalALT  49227  precofcl  49229  termcfuncval  49365