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 690	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1541  (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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414

This theorem is referenced by:  oveq123i  7425  caovdir  7643  caovdilem  7644  caovlem2  7645  cnfcom2  9699  canthwelem  10647  adderpqlem  10951  addassnq  10955  distrnq  10958  ltanq  10968  1lt2nq  10970  ltexnq  10972  halfnq  10973  mulcmpblnrlem  11067  mulcomsr  11086  distrsr  11088  m1p1sr  11089  m1m1sr  11090  mulgt0sr  11102  addcnsrec  11140  mulcnsrec  11141  axmulcom  11152  axmulass  11154  axdistr  11155  axi2m1  11156  addrid  11398  3t3e9  12383  8th4div3  12436  halfpm6th  12437  numma  12725  decmul10add  12750  4t3lem  12778  9t11e99  12811  halfthird  12824  5recm6rec  12825  fz0to3un2pr  13607  seqfeq4  14021  seqof  14029  sqdivi  14153  sq4e2t8  14167  i4  14172  binom2i  14180  nn0opthlem1  14232  facp1  14242  fac2  14243  fac3  14244  fac4  14245  faclbnd4lem1  14257  4bc2eq6  14293  ccat2s1len  14577  ccat2s1p2  14584  cats1len  14815  cats2cat  14817  ofs2  14922  cji  15110  01sqrexlem5  15197  fsumadd  15690  fsumsplitf  15692  fsumsplitsnun  15705  0.999...  15831  fprodmul  15908  fproddiv  15909  fprodsplitf  15936  bpoly3  16006  fsumcube  16008  efsep  16057  ef01bndlem  16131  cos2bnd  16135  rpnnen2lem3  16163  3dvds2dec  16280  flodddiv4  16360  sadeq  16417  gcdaddmlem  16469  bezout  16489  nn0gcdsq  16692  pythagtriplem16  16767  4sqlem19  16900  dec5nprm  17003  dec2nprm  17004  mod2xnegi  17008  numexp2x  17016  decsplit  17020  karatsuba  17021  2exp5  17023  2exp11  17027  2exp16  17028  37prm  17058  43prm  17059  83prm  17060  139prm  17061  163prm  17062  317prm  17063  631prm  17064  1259lem1  17068  1259lem2  17069  1259lem3  17070  1259lem4  17071  1259lem5  17072  1259prm  17073  2503lem1  17074  2503lem2  17075  2503lem3  17076  2503prm  17077  4001lem1  17078  4001lem2  17079  4001lem3  17080  4001lem4  17081  4001prm  17082  funcoppc  17829  estrchom  18082  funcestrcsetclem5  18100  yonedalem3b  18236  ecqusaddd  19107  symgressbas  19290  gsum2dlem2  19880  opprrng  20236  isrhm  20369  rngqiprnglinlem2  21051  pzriprng1ALT  21265  evlsval  21868  mamudi  22123  mamudir  22124  oftpos  22174  mamutpos  22180  mdetrlin  22324  mdetrlin2  22329  mdetunilem5  22338  cpmadugsumfi  22599  cnmpt2res  23401  ussval  23984  icopnfhmeo  24683  iccpnfhmeo  24685  pcoass  24764  ovolunlem1a  25237  ioombl1lem3  25301  ioombl1lem4  25302  mbfimaopnlem  25396  itgfsum  25568  iblabslem  25569  itgsplit  25577  dveflem  25720  efhalfpi  26205  efipi  26207  sin2pi  26209  ef2pi  26211  sincosq3sgn  26234  sincosq4sgn  26235  sinq34lt0t  26243  sincos4thpi  26247  tan4thpi  26248  sincos6thpi  26249  sincos3rdpi  26250  pigt3  26251  pige3ALT  26253  cxpcn3  26480  lawcos  26545  1cubrlem  26570  quart1lem  26584  quart1  26585  asin1  26623  atancj  26639  atanlogsublem  26644  log2cnv  26673  log2tlbnd  26674  log2ublem3  26677  log2ub  26678  birthday  26683  basellem8  26816  basellem9  26817  cht2  26900  cht3  26901  1sgm2ppw  26927  bclbnd  27007  bposlem8  27018  bposlem9  27019  lgsdi  27061  lgsquadlem1  27107  2lgsoddprmlem3c  27139  2lgsoddprmlem3d  27140  addsqnreup  27170  addsval2  27673  addsunif  27712  addsasslem1  27713  addsasslem2  27714  negsval  27727  negs0s  27728  negsid  27742  mulsval2  27794  muls01  27795  mulsproplem2  27800  mulsproplem3  27801  mulsproplem4  27802  mulsproplem5  27803  mulsproplem6  27804  mulsproplem7  27805  mulsproplem8  27806  mulsproplem12  27810  mulsproplem13  27811  mulsproplem14  27812  mulsunif  27832  addsdilem1  27833  addsdilem2  27834  mulsasslem1  27845  mulsasslem2  27846  precsexlem11  27890  mirauto  28190  axsegconlem9  28438  ax5seglem7  28448  vtxdginducedm1  29055  clwlkclwwlkfo  29517  eupth2eucrct  29725  ex-exp  29958  ex-fac  29959  ex-bc  29960  ex-hash  29961  ip0i  30333  ip1ilem  30334  ip2i  30336  ipdirilem  30337  ipasslem10  30347  ip2dii  30352  pythi  30358  siilem1  30359  hvsubsub4i  30567  hvsubcan2i  30572  hisubcomi  30612  normlem0  30617  normlem1  30618  normlem2  30619  normlem3  30620  normlem6  30623  normlem8  30625  normlem9  30626  bcseqi  30628  norm-ii-i  30645  norm-iii-i  30647  normpythi  30650  norm3difi  30655  normpari  30662  normpar2i  30664  polid2i  30665  polidi  30666  bcsiALT  30687  lediri  31045  h1de2i  31061  cmcmlem  31099  cmbr2i  31104  cm2j  31128  fh3i  31131  fh4i  31132  pjaddii  31183  pjsslem  31187  pjssmii  31189  pjdifnormii  31191  lnopeq0lem1  31513  lnopunilem1  31518  lnophmlem2  31525  pjsdi2i  31665  pjclem1  31703  golem1  31779  dpmul100  32318  dpmul1000  32320  dpadd2  32331  dpadd  32332  dpadd3  32333  dpmul  32334  dpmul4  32335  gsumle  32500  matdim  32976  rmulccn  33194  raddcn  33195  xrmulc1cn  33196  xrge0iifhmeo  33202  qqh0  33250  qqh1  33251  elmbfmvol2  33552  mbfmcnt  33553  eulerpartlemgvv  33661  eulerpartlemgh  33663  fib2  33687  fib3  33688  fib4  33689  fib5  33690  fib6  33691  ballotlem2  33773  ballotlemfval0  33780  ballotth  33822  hgt750lem2  33950  problem2  34937  problem4  34939  quad3  34941  gg-rmulccn  35465  poimirlem30  36821  iblabsnclem  36854  dalem10  38847  cdleme0e  39391  cdleme7c  39419  cdleme20c  39485  3exp7  41224  3lexlogpow5ineq1  41225  3lexlogpow5ineq5  41231  aks4d1p1  41247  5bc2eq10  41264  sn-1ne2  41481  sqmid3api  41497  sqdeccom12  41503  sq3deccom12  41504  nn0expgcd  41528  rei4  41598  ipiiie0  41612  sn-0tie0  41614  mzpcompact2lem  41791  pellexlem5  41873  pellfundgt1  41923  jm2.27c  42048  areaquad  42267  resqrtvalex  42698  imsqrtvalex  42699  lhe4.4ex1a  43390  mccl  44613  dvnprodlem2  44962  itgsin0pilem1  44965  stoweidlem13  45028  wallispilem4  45083  wallispi2lem1  45086  wallispi2lem2  45087  dirkerper  45111  dirkertrigeqlem1  45113  fourierdlem30  45152  fourierdlem47  45168  fourierdlem103  45224  fourierdlem104  45225  fouriersw  45246  etransclem37  45286  sge0splitmpt  45426  sge0xaddlem2  45449  sge0xadd  45450  caragen0  45521  caragenuncllem  45527  fsumsplitsndif  46340  139prmALT  46563  127prm  46566  m11nprm  46568  3exp4mod41  46583  sbgoldbo  46754  2t6m3t4e0  47113  lincsum  47198  zlmodzxzequa  47265  zlmodzxzequap  47268  zlmodzxzldeplem3  47271  rrx2linest  47516  line2  47526  itsclc0yqsollem1  47536  itsclquadb  47550  itscnhlinecirc02plem2  47557