Theorem oveq12i 7361

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveq123i  7363  caovdir  7583  caovdilem  7584  caovlem2  7585  cnfcom2  9598  canthwelem  10544  adderpqlem  10848  addassnq  10852  distrnq  10855  ltanq  10865  1lt2nq  10867  ltexnq  10869  halfnq  10870  mulcmpblnrlem  10964  mulcomsr  10983  distrsr  10985  m1p1sr  10986  m1m1sr  10987  mulgt0sr  10999  addcnsrec  11037  mulcnsrec  11038  axmulcom  11049  axmulass  11051  axdistr  11052  axi2m1  11053  addrid  11296  3t3e9  12290  8th4div3  12344  halfthird  12345  numma  12635  decmul10add  12660  4t3lem  12688  9t11e99  12721  5recm6rec  12734  fz0to3un2pr  13532  seqfeq4  13958  seqof  13966  sqdivi  14092  sq4e2t8  14106  i4  14111  binom2i  14119  nn0opthlem1  14175  facp1  14185  fac2  14186  fac3  14187  fac4  14188  faclbnd4lem1  14200  4bc2eq6  14236  ccat2s1len  14530  ccat2s1p2  14537  cats1len  14767  cats2cat  14769  ofs2  14878  cji  15066  01sqrexlem5  15153  fsumadd  15647  fsumsplitf  15649  fsumsplitsnun  15662  0.999...  15788  fprodmul  15867  fproddiv  15868  fprodsplitf  15895  bpoly3  15965  fsumcube  15967  efsep  16019  ef01bndlem  16093  cos2bnd  16097  rpnnen2lem3  16125  3dvds2dec  16244  flodddiv4  16326  sadeq  16383  gcdaddmlem  16435  bezout  16454  nn0expgcd  16475  nn0gcdsq  16663  pythagtriplem16  16742  4sqlem19  16875  dec5nprm  16978  dec2nprm  16979  mod2xnegi  16983  numexp2x  16990  decsplit  16994  karatsuba  16995  2exp5  16997  2exp11  17001  2exp16  17002  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  funcoppc  17782  estrchom  18033  funcestrcsetclem5  18050  yonedalem3b  18185  ecqusaddd  19071  symgressbas  19261  gsum2dlem2  19850  gsumle  20024  opprrng  20230  isrhm  20363  rngqiprnglinlem2  21199  pzriprng1ALT  21403  evlsval  21991  mamudi  22288  mamudir  22289  oftpos  22337  mamutpos  22343  mdetrlin  22487  mdetrlin2  22492  mdetunilem5  22501  cpmadugsumfi  22762  cnmpt2res  23562  ussval  24145  icopnfhmeo  24839  iccpnfhmeo  24841  pcoass  24922  ovolunlem1a  25395  ioombl1lem3  25459  ioombl1lem4  25460  mbfimaopnlem  25554  itgfsum  25726  iblabslem  25727  itgsplit  25735  dveflem  25881  efhalfpi  26378  efipi  26380  sin2pi  26382  ef2pi  26384  sincosq3sgn  26407  sincosq4sgn  26408  sinq34lt0t  26416  sincos4thpi  26420  tan4thpi  26421  tan4thpiOLD  26422  sincos6thpi  26423  sincos3rdpi  26424  pigt3  26425  pige3ALT  26427  cxpcn3  26656  lawcos  26724  1cubrlem  26749  quart1lem  26763  quart1  26764  asin1  26802  atancj  26818  atanlogsublem  26823  log2cnv  26852  log2tlbnd  26853  log2ublem3  26856  log2ub  26857  birthday  26862  basellem8  26996  basellem9  26997  cht2  27080  cht3  27081  1sgm2ppw  27109  bclbnd  27189  bposlem8  27200  bposlem9  27201  lgsdi  27243  lgsquadlem1  27289  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  addsqnreup  27352  addsval2  27875  addsunif  27914  addsasslem1  27915  addsasslem2  27916  negsval  27936  negs0s  27937  negs1s  27938  negsid  27952  mulsval2  28019  muls01  28020  mulsproplem2  28025  mulsproplem3  28026  mulsproplem4  28027  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  mulsunif  28058  addsdilem1  28059  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  mulsunif2  28078  precsexlem11  28124  onmulscl  28180  1p1e2s  28308  twocut  28315  0reno  28366  mirauto  28629  axsegconlem9  28870  ax5seglem7  28880  vtxdginducedm1  29489  clwlkclwwlkfo  29953  eupth2eucrct  30161  ex-exp  30394  ex-fac  30395  ex-bc  30396  ex-hash  30397  ip0i  30769  ip1ilem  30770  ip2i  30772  ipdirilem  30773  ipasslem10  30783  ip2dii  30788  pythi  30794  siilem1  30795  hvsubsub4i  31003  hvsubcan2i  31008  hisubcomi  31048  normlem0  31053  normlem1  31054  normlem2  31055  normlem3  31056  normlem6  31059  normlem8  31061  normlem9  31062  bcseqi  31064  norm-ii-i  31081  norm-iii-i  31083  normpythi  31086  norm3difi  31091  normpari  31098  normpar2i  31100  polid2i  31101  polidi  31102  bcsiALT  31123  lediri  31481  h1de2i  31497  cmcmlem  31535  cmbr2i  31540  cm2j  31564  fh3i  31567  fh4i  31568  pjaddii  31619  pjsslem  31623  pjssmii  31625  pjdifnormii  31627  lnopeq0lem1  31949  lnopunilem1  31954  lnophmlem2  31961  pjsdi2i  32101  pjclem1  32139  golem1  32215  dpmul100  32838  dpmul1000  32840  dpadd2  32851  dpadd  32852  dpadd3  32853  dpmul  32854  dpmul4  32855  ccatws1f1o  32894  elrgspnlem2  33184  matdim  33588  fldext2chn  33701  constrextdg2lem  33721  constrext2chnlem  33723  iconstr  33739  cos9thpiminplylem4  33758  cos9thpiminplylem5  33759  rmulccn  33901  raddcn  33902  xrmulc1cn  33903  xrge0iifhmeo  33909  qqh0  33957  qqh1  33958  elmbfmvol2  34241  mbfmcnt  34242  eulerpartlemgvv  34350  eulerpartlemgh  34352  fib2  34376  fib3  34377  fib4  34378  fib5  34379  fib6  34380  ballotlem2  34463  ballotlemfval0  34470  ballotth  34512  hgt750lem2  34626  problem2  35649  problem4  35651  quad3  35653  ditgeq123i  36193  cbvditgvw2  36233  poimirlem30  37640  iblabsnclem  37673  dalem10  39662  cdleme0e  40206  cdleme7c  40234  cdleme20c  40300  3exp7  42036  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1  42059  5bc2eq10  42125  aks5lem3a  42172  sn-1ne2  42248  sqmid3api  42266  sqdeccom12  42272  sq3deccom12  42273  tan3rdpi  42335  sin2t3rdpi  42336  cos2t3rdpi  42337  rei4  42407  ipiiie0  42421  sn-0tie0  42434  mzpcompact2lem  42734  pellexlem5  42816  pellfundgt1  42866  jm2.27c  42990  areaquad  43199  resqrtvalex  43628  imsqrtvalex  43629  lhe4.4ex1a  44312  mccl  45589  dvnprodlem2  45938  itgsin0pilem1  45941  stoweidlem13  46004  wallispilem4  46059  wallispi2lem1  46062  wallispi2lem2  46063  dirkerper  46087  dirkertrigeqlem1  46089  fourierdlem30  46128  fourierdlem47  46144  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem37  46262  sge0splitmpt  46402  sge0xaddlem2  46425  sge0xadd  46426  caragen0  46497  caragenuncllem  46503  fsumsplitsndif  47367  139prmALT  47590  127prm  47593  m11nprm  47595  3exp4mod41  47610  sbgoldbo  47781  2t6m3t4e0  48342  lincsum  48424  zlmodzxzequa  48491  zlmodzxzequap  48494  zlmodzxzldeplem3  48497  rrx2linest  48737  line2  48747  itsclc0yqsollem1  48757  itsclquadb  48771  itscnhlinecirc02plem2  48778  postcofval  49359  postcofcl  49360  precofval  49362  precofvalALT  49363  precofcl  49365  termcfuncval  49527