Theorem oveq12i 7443

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  oveq123i  7445  caovdir  7667  caovdilem  7668  caovlem2  7669  cnfcom2  9742  canthwelem  10690  adderpqlem  10994  addassnq  10998  distrnq  11001  ltanq  11011  1lt2nq  11013  ltexnq  11015  halfnq  11016  mulcmpblnrlem  11110  mulcomsr  11129  distrsr  11131  m1p1sr  11132  m1m1sr  11133  mulgt0sr  11145  addcnsrec  11183  mulcnsrec  11184  axmulcom  11195  axmulass  11197  axdistr  11198  axi2m1  11199  addrid  11441  3t3e9  12433  8th4div3  12486  halfpm6th  12487  numma  12777  decmul10add  12802  4t3lem  12830  9t11e99  12863  halfthird  12876  5recm6rec  12877  fz0to3un2pr  13669  seqfeq4  14092  seqof  14100  sqdivi  14224  sq4e2t8  14238  i4  14243  binom2i  14251  nn0opthlem1  14307  facp1  14317  fac2  14318  fac3  14319  fac4  14320  faclbnd4lem1  14332  4bc2eq6  14368  ccat2s1len  14661  ccat2s1p2  14668  cats1len  14899  cats2cat  14901  ofs2  15010  cji  15198  01sqrexlem5  15285  fsumadd  15776  fsumsplitf  15778  fsumsplitsnun  15791  0.999...  15917  fprodmul  15996  fproddiv  15997  fprodsplitf  16024  bpoly3  16094  fsumcube  16096  efsep  16146  ef01bndlem  16220  cos2bnd  16224  rpnnen2lem3  16252  3dvds2dec  16370  flodddiv4  16452  sadeq  16509  gcdaddmlem  16561  bezout  16580  nn0expgcd  16601  nn0gcdsq  16789  pythagtriplem16  16868  4sqlem19  17001  dec5nprm  17104  dec2nprm  17105  mod2xnegi  17109  numexp2x  17116  decsplit  17120  karatsuba  17121  2exp5  17123  2exp11  17127  2exp16  17128  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  funcoppc  17920  estrchom  18171  funcestrcsetclem5  18189  yonedalem3b  18324  ecqusaddd  19210  symgressbas  19399  gsum2dlem2  19989  opprrng  20345  isrhm  20478  rngqiprnglinlem2  21302  pzriprng1ALT  21507  evlsval  22110  mamudi  22407  mamudir  22408  oftpos  22458  mamutpos  22464  mdetrlin  22608  mdetrlin2  22613  mdetunilem5  22622  cpmadugsumfi  22883  cnmpt2res  23685  ussval  24268  icopnfhmeo  24974  iccpnfhmeo  24976  pcoass  25057  ovolunlem1a  25531  ioombl1lem3  25595  ioombl1lem4  25596  mbfimaopnlem  25690  itgfsum  25862  iblabslem  25863  itgsplit  25871  dveflem  26017  efhalfpi  26513  efipi  26515  sin2pi  26517  ef2pi  26519  sincosq3sgn  26542  sincosq4sgn  26543  sinq34lt0t  26551  sincos4thpi  26555  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  sincos3rdpi  26559  pigt3  26560  pige3ALT  26562  cxpcn3  26791  lawcos  26859  1cubrlem  26884  quart1lem  26898  quart1  26899  asin1  26937  atancj  26953  atanlogsublem  26958  log2cnv  26987  log2tlbnd  26988  log2ublem3  26991  log2ub  26992  birthday  26997  basellem8  27131  basellem9  27132  cht2  27215  cht3  27216  1sgm2ppw  27244  bclbnd  27324  bposlem8  27335  bposlem9  27336  lgsdi  27378  lgsquadlem1  27424  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  addsqnreup  27487  addsval2  27996  addsunif  28035  addsasslem1  28036  addsasslem2  28037  negsval  28057  negs0s  28058  negs1s  28059  negsid  28073  mulsval2  28137  muls01  28138  mulsproplem2  28143  mulsproplem3  28144  mulsproplem4  28145  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  mulsunif  28176  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  mulsunif2  28196  precsexlem11  28241  onmulscl  28287  1p1e2s  28400  nohalf  28407  0reno  28429  mirauto  28692  axsegconlem9  28940  ax5seglem7  28950  vtxdginducedm1  29561  clwlkclwwlkfo  30028  eupth2eucrct  30236  ex-exp  30469  ex-fac  30470  ex-bc  30471  ex-hash  30472  ip0i  30844  ip1ilem  30845  ip2i  30847  ipdirilem  30848  ipasslem10  30858  ip2dii  30863  pythi  30869  siilem1  30870  hvsubsub4i  31078  hvsubcan2i  31083  hisubcomi  31123  normlem0  31128  normlem1  31129  normlem2  31130  normlem3  31131  normlem6  31134  normlem8  31136  normlem9  31137  bcseqi  31139  norm-ii-i  31156  norm-iii-i  31158  normpythi  31161  norm3difi  31166  normpari  31173  normpar2i  31175  polid2i  31176  polidi  31177  bcsiALT  31198  lediri  31556  h1de2i  31572  cmcmlem  31610  cmbr2i  31615  cm2j  31639  fh3i  31642  fh4i  31643  pjaddii  31694  pjsslem  31698  pjssmii  31700  pjdifnormii  31702  lnopeq0lem1  32024  lnopunilem1  32029  lnophmlem2  32036  pjsdi2i  32176  pjclem1  32214  golem1  32290  dpmul100  32879  dpmul1000  32881  dpadd2  32892  dpadd  32893  dpadd3  32894  dpmul  32895  dpmul4  32896  ccatws1f1o  32936  gsumle  33101  elrgspnlem2  33247  matdim  33666  fldext2chn  33769  constrextdg2lem  33789  rmulccn  33927  raddcn  33928  xrmulc1cn  33929  xrge0iifhmeo  33935  qqh0  33985  qqh1  33986  elmbfmvol2  34269  mbfmcnt  34270  eulerpartlemgvv  34378  eulerpartlemgh  34380  fib2  34404  fib3  34405  fib4  34406  fib5  34407  fib6  34408  ballotlem2  34491  ballotlemfval0  34498  ballotth  34540  hgt750lem2  34667  problem2  35671  problem4  35673  quad3  35675  ditgeq123i  36210  cbvditgvw2  36250  poimirlem30  37657  iblabsnclem  37690  dalem10  39675  cdleme0e  40219  cdleme7c  40247  cdleme20c  40313  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1  42077  5bc2eq10  42143  aks5lem3a  42190  sn-1ne2  42300  sqmid3api  42318  sqdeccom12  42324  sq3deccom12  42325  tan3rdpi  42386  rei4  42453  ipiiie0  42467  sn-0tie0  42469  mzpcompact2lem  42762  pellexlem5  42844  pellfundgt1  42894  jm2.27c  43019  areaquad  43228  resqrtvalex  43658  imsqrtvalex  43659  lhe4.4ex1a  44348  mccl  45613  dvnprodlem2  45962  itgsin0pilem1  45965  stoweidlem13  46028  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  dirkerper  46111  dirkertrigeqlem1  46113  fourierdlem30  46152  fourierdlem47  46168  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  etransclem37  46286  sge0splitmpt  46426  sge0xaddlem2  46449  sge0xadd  46450  caragen0  46521  caragenuncllem  46527  fsumsplitsndif  47360  139prmALT  47583  127prm  47586  m11nprm  47588  3exp4mod41  47603  sbgoldbo  47774  2t6m3t4e0  48264  lincsum  48346  zlmodzxzequa  48413  zlmodzxzequap  48416  zlmodzxzldeplem3  48419  rrx2linest  48663  line2  48673  itsclc0yqsollem1  48683  itsclquadb  48697  itscnhlinecirc02plem2  48704  postcofval  49059  postcofcl  49060  precofval  49062  precofvalALT  49063  precofcl  49065