Theorem oveq12i 7379

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

Syntax hints:   = wceq 1542  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  oveq123i  7381  caovdir  7601  caovdilem  7602  caovlem2  7603  cnfcom2  9623  canthwelem  10573  adderpqlem  10877  addassnq  10881  distrnq  10884  ltanq  10894  1lt2nq  10896  ltexnq  10898  halfnq  10899  mulcmpblnrlem  10993  mulcomsr  11012  distrsr  11014  m1p1sr  11015  m1m1sr  11016  mulgt0sr  11028  addcnsrec  11066  mulcnsrec  11067  axmulcom  11078  axmulass  11080  axdistr  11081  axi2m1  11082  addrid  11326  3t3e9  12343  8th4div3  12397  halfthird  12398  numma  12688  decmul10add  12713  4t3lem  12741  9t11e99  12774  5recm6rec  12787  fz0to3un2pr  13583  seqfeq4  14013  seqof  14021  sqdivi  14147  sq4e2t8  14161  i4  14166  binom2i  14174  nn0opthlem1  14230  facp1  14240  fac2  14241  fac3  14242  fac4  14243  faclbnd4lem1  14255  4bc2eq6  14291  ccat2s1len  14586  ccat2s1p2  14593  cats1len  14822  cats2cat  14824  ofs2  14933  cji  15121  01sqrexlem5  15208  fsumadd  15702  fsumsplitf  15704  fsumsplitsnun  15717  0.999...  15846  fprodmul  15925  fproddiv  15926  fprodsplitf  15953  bpoly3  16023  fsumcube  16025  efsep  16077  ef01bndlem  16151  cos2bnd  16155  rpnnen2lem3  16183  3dvds2dec  16302  flodddiv4  16384  sadeq  16441  gcdaddmlem  16493  bezout  16512  nn0expgcd  16533  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  17842  estrchom  18093  funcestrcsetclem5  18110  yonedalem3b  18245  ecqusaddd  19167  symgressbas  19357  gsum2dlem2  19946  gsumle  20120  opprrng  20325  isrhm  20458  rngqiprnglinlem2  21290  pzriprng1ALT  21476  evlsval  22064  mamudi  22368  mamudir  22369  oftpos  22417  mamutpos  22423  mdetrlin  22567  mdetrlin2  22572  mdetunilem5  22581  cpmadugsumfi  22842  cnmpt2res  23642  ussval  24224  icopnfhmeo  24910  iccpnfhmeo  24912  pcoass  24991  ovolunlem1a  25463  ioombl1lem3  25527  ioombl1lem4  25528  mbfimaopnlem  25622  itgfsum  25794  iblabslem  25795  itgsplit  25803  dveflem  25946  efhalfpi  26435  efipi  26437  sin2pi  26439  ef2pi  26441  sincosq3sgn  26464  sincosq4sgn  26465  sinq34lt0t  26473  sincos4thpi  26477  tan4thpi  26478  tan4thpiOLD  26479  sincos6thpi  26480  sincos3rdpi  26481  pigt3  26482  pige3ALT  26484  cxpcn3  26712  lawcos  26780  1cubrlem  26805  quart1lem  26819  quart1  26820  asin1  26858  atancj  26874  atanlogsublem  26879  log2cnv  26908  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  birthday  26918  basellem8  27051  basellem9  27052  cht2  27135  cht3  27136  1sgm2ppw  27163  bclbnd  27243  bposlem8  27254  bposlem9  27255  lgsdi  27297  lgsquadlem1  27343  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  addsqnreup  27406  addsval2  27955  addsunif  27994  addsasslem1  27995  addsasslem2  27996  negsval  28017  neg0s  28018  neg1s  28019  negsid  28033  mulsval2  28103  muls01  28104  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsunif  28142  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  mulsunif2  28162  precsexlem11  28209  onmulscl  28270  twocut  28415  mirauto  28752  axsegconlem9  28994  ax5seglem7  29004  vtxdginducedm1  29612  clwlkclwwlkfo  30079  eupth2eucrct  30287  ex-exp  30520  ex-fac  30521  ex-bc  30522  ex-hash  30523  ip0i  30896  ip1ilem  30897  ip2i  30899  ipdirilem  30900  ipasslem10  30910  ip2dii  30915  pythi  30921  siilem1  30922  hvsubsub4i  31130  hvsubcan2i  31135  hisubcomi  31175  normlem0  31180  normlem1  31181  normlem2  31182  normlem3  31183  normlem6  31186  normlem8  31188  normlem9  31189  bcseqi  31191  norm-ii-i  31208  norm-iii-i  31210  normpythi  31213  norm3difi  31218  normpari  31225  normpar2i  31227  polid2i  31228  polidi  31229  bcsiALT  31250  lediri  31608  h1de2i  31624  cmcmlem  31662  cmbr2i  31667  cm2j  31691  fh3i  31694  fh4i  31695  pjaddii  31746  pjsslem  31750  pjssmii  31752  pjdifnormii  31754  lnopeq0lem1  32076  lnopunilem1  32081  lnophmlem2  32088  pjsdi2i  32228  pjclem1  32266  golem1  32342  dpmul100  32956  dpmul1000  32958  dpadd2  32969  dpadd  32970  dpadd3  32971  dpmul  32972  dpmul4  32973  ccatws1f1o  33011  elrgspnlem2  33304  matdim  33759  fldext2chn  33872  constrextdg2lem  33892  constrext2chnlem  33894  iconstr  33910  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  rmulccn  34072  raddcn  34073  xrmulc1cn  34074  xrge0iifhmeo  34080  qqh0  34128  qqh1  34129  elmbfmvol2  34411  mbfmcnt  34412  eulerpartlemgvv  34520  eulerpartlemgh  34522  fib2  34546  fib3  34547  fib4  34548  fib5  34549  fib6  34550  ballotlem2  34633  ballotlemfval0  34640  ballotth  34682  hgt750lem2  34796  problem2  35848  problem4  35850  quad3  35852  ditgeq123i  36391  cbvditgvw2  36431  poimirlem30  37971  iblabsnclem  38004  dalem10  40119  cdleme0e  40663  cdleme7c  40691  cdleme20c  40757  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1  42515  5bc2eq10  42581  aks5lem3a  42628  sn-1ne2  42703  sqmid3api  42715  sqdeccom12  42721  sq3deccom12  42722  tan3rdpi  42784  sin2t3rdpi  42785  cos2t3rdpi  42786  rei4  42856  ipiiie0  42870  sn-0tie0  42896  mzpcompact2lem  43183  pellexlem5  43261  pellfundgt1  43311  jm2.27c  43435  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  lhe4.4ex1a  44756  mccl  46028  dvnprodlem2  46375  itgsin0pilem1  46378  stoweidlem13  46441  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  dirkerper  46524  dirkertrigeqlem1  46526  fourierdlem30  46565  fourierdlem47  46581  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  etransclem37  46699  sge0splitmpt  46839  sge0xaddlem2  46862  sge0xadd  46863  caragen0  46934  caragenuncllem  46940  nthrucw  47316  goldrasin  47330  goldratmolem2  47334  fsumsplitsndif  47829  139prmALT  48059  127prm  48062  m11nprm  48064  3exp4mod41  48079  ppivalnn4  48090  sbgoldbo  48263  2t6m3t4e0  48824  lincsum  48905  zlmodzxzequa  48972  zlmodzxzequap  48975  zlmodzxzldeplem3  48978  rrx2linest  49218  line2  49228  itsclc0yqsollem1  49238  itsclquadb  49252  itscnhlinecirc02plem2  49259  postcofval  49839  postcofcl  49840  precofval  49842  precofvalALT  49843  precofcl  49845  termcfuncval  50007