Theorem oveq12i 7410

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

Syntax hints:   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  oveq123i  7412  caovdir  7632  caovdilem  7633  caovlem2  7634  cnfcom2  9659  canthwelem  10610  adderpqlem  10914  addassnq  10918  distrnq  10921  ltanq  10931  1lt2nq  10933  ltexnq  10935  halfnq  10936  mulcmpblnrlem  11030  mulcomsr  11049  distrsr  11051  m1p1sr  11052  m1m1sr  11053  mulgt0sr  11065  addcnsrec  11103  mulcnsrec  11104  axmulcom  11115  axmulass  11117  axdistr  11118  axi2m1  11119  addrid  11365  3t3e9  12387  8th4div3  12443  halfthird  12444  numma  12739  decmul10add  12764  4t3lem  12792  9t11e99OLD  12826  5recm6rec  12840  fz0to3un2pr  13636  seqfeq4  14066  seqof  14074  sqdivi  14200  sq4e2t8  14214  i4  14219  binom2i  14227  nn0opthlem1  14283  facp1  14293  fac2  14294  fac3  14295  fac4  14296  faclbnd4lem1  14308  4bc2eq6  14344  ccat2s1len  14639  ccat2s1p2  14646  cats1len  14875  cats2cat  14877  ofs2  14986  cji  15188  01sqrexlem5  15275  fsumadd  15769  fsumsplitf  15771  fsumsplitsnun  15784  0.999...  15913  fprodmul  15992  fproddiv  15993  fprodsplitf  16020  bpoly3  16090  fsumcube  16092  efsep  16144  ef01bndlem  16218  cos2bnd  16222  rpnnen2lem3  16250  3dvds2dec  16369  flodddiv4  16451  sadeq  16508  gcdaddmlem  16560  bezout  16579  nn0expgcd  16600  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  17159  43prm  17160  83prm  17161  139prm  17162  163prm  17163  317prm  17164  631prm  17165  1259lem1  17169  1259lem2  17170  1259lem3  17171  1259lem4  17172  1259lem5  17173  1259prm  17174  2503lem1  17175  2503lem2  17176  2503lem3  17177  2503prm  17178  4001lem1  17179  4001lem2  17180  4001lem3  17181  4001lem4  17182  4001prm  17183  funcoppc  17910  estrchom  18161  funcestrcsetclem5  18178  yonedalem3b  18313  ecqusaddd  19235  symgressbas  19424  gsum2dlem2  20013  gsumle  20187  opprrng  20396  isrhm  20529  rngqiprnglinlem2  21364  pzriprng1ALT  21550  evlsval  22141  mamudi  22465  mamudir  22466  oftpos  22514  mamutpos  22520  mdetrlin  22664  mdetrlin2  22669  mdetunilem5  22678  cpmadugsumfi  22939  cnmpt2res  23739  ussval  24321  icopnfhmeo  25007  iccpnfhmeo  25009  pcoass  25088  ovolunlem1a  25560  ioombl1lem3  25624  ioombl1lem4  25625  mbfimaopnlem  25719  itgfsum  25891  iblabslem  25892  itgsplit  25900  dveflem  26043  efhalfpi  26538  efipi  26540  sin2pi  26542  ef2pi  26544  sincosq3sgn  26567  sincosq4sgn  26568  sinq34lt0t  26576  sincos4thpi  26580  tan4thpi  26581  tan4thpiOLD  26582  sincos6thpi  26583  sincos3rdpi  26584  pigt3  26585  pige3ALT  26587  cxpcn3  26815  lawcos  26883  1cubrlem  26908  quart1lem  26922  quart1  26923  asin1  26961  atancj  26977  atanlogsublem  26982  log2cnv  27011  log2tlbnd  27012  log2ublem3  27015  log2ub  27016  birthday  27021  basellem8  27154  basellem9  27155  cht2  27238  cht3  27239  1sgm2ppw  27266  bclbnd  27346  bposlem8  27357  bposlem9  27358  lgsdi  27400  lgsquadlem1  27446  2lgsoddprmlem3c  27478  2lgsoddprmlem3d  27479  addsqnreup  27509  addsval2  28058  addsunif  28097  addsasslem1  28098  addsasslem2  28099  negsval  28120  neg0s  28121  neg1s  28122  negsid  28136  mulsval2  28206  muls01  28207  mulsproplem2  28212  mulsproplem3  28213  mulsproplem4  28214  mulsproplem5  28215  mulsproplem6  28216  mulsproplem7  28217  mulsproplem8  28218  mulsproplem12  28222  mulsproplem13  28223  mulsproplem14  28224  mulsunif  28245  addsdilem1  28246  addsdilem2  28247  mulsasslem1  28258  mulsasslem2  28259  mulsunif2  28265  precsexlem11  28312  onmulscl  28373  twocut  28518  mirauto  28859  axsegconlem9  29128  ax5seglem7  29138  vtxdginducedm1  29746  clwlkclwwlkfo  30213  eupth2eucrct  30421  ex-exp  30654  ex-fac  30655  ex-bc  30656  ex-hash  30657  ip0i  31030  ip1ilem  31031  ip2i  31033  ipdirilem  31034  ipasslem10  31044  ip2dii  31049  pythi  31055  siilem1  31056  hvsubsub4i  31264  hvsubcan2i  31269  hisubcomi  31309  normlem0  31314  normlem1  31315  normlem2  31316  normlem3  31317  normlem6  31320  normlem8  31322  normlem9  31323  bcseqi  31325  norm-ii-i  31342  norm-iii-i  31344  normpythi  31347  norm3difi  31352  normpari  31359  normpar2i  31361  polid2i  31362  polidi  31363  bcsiALT  31384  lediri  31742  h1de2i  31758  cmcmlem  31796  cmbr2i  31801  cm2j  31825  fh3i  31828  fh4i  31829  pjaddii  31880  pjsslem  31884  pjssmii  31886  pjdifnormii  31888  lnopeq0lem1  32210  lnopunilem1  32215  lnophmlem2  32222  pjsdi2i  32362  pjclem1  32400  golem1  32476  dpmul100  33076  dpmul1000  33078  dpadd2  33089  dpadd  33090  dpadd3  33091  dpmul  33092  dpmul4  33093  ccatws1f1o  33131  elrgspnlem2  33426  matdim  33914  fldext2chn  34027  constrextdg2lem  34047  constrext2chnlem  34049  iconstr  34065  cos9thpiminplylem4  34084  cos9thpiminplylem5  34085  rmulccn  34227  raddcn  34228  xrmulc1cn  34229  xrge0iifhmeo  34235  qqh0  34283  qqh1  34284  elmbfmvol2  34566  mbfmcnt  34567  eulerpartlemgvv  34675  eulerpartlemgh  34677  fib2  34701  fib3  34702  fib4  34703  fib5  34704  fib6  34705  ballotlem2  34788  ballotlemfval0  34795  ballotth  34837  hgt750lem2  34948  problem2  36021  problem4  36023  quad3  36025  ditgeq123i  36574  cbvditgvw2  36614  poimirlem30  38154  iblabsnclem  38187  dalem10  40302  cdleme0e  40846  cdleme7c  40874  cdleme20c  40940  3exp7  42675  3lexlogpow5ineq1  42676  3lexlogpow5ineq5  42682  aks4d1p1  42698  5bc2eq10  42764  aks5lem3a  42811  sn-1ne2  42885  sqmid3api  42897  sqdeccom12  42903  sq3deccom12  42904  tan3rdpi  42966  sin2t3rdpi  42967  cos2t3rdpi  42968  rei4  43038  ipiiie0  43052  sn-0tie0  43078  mzpcompact2lem  43337  pellexlem5  43415  pellfundgt1  43465  jm2.27c  43589  areaquad  43798  resqrtvalex  44226  imsqrtvalex  44227  lhe4.4ex1a  44910  mccl  46179  dvnprodlem2  46526  itgsin0pilem1  46529  stoweidlem13  46592  wallispilem4  46647  wallispi2lem1  46650  wallispi2lem2  46651  dirkerper  46675  dirkertrigeqlem1  46677  fourierdlem30  46716  fourierdlem47  46732  fourierdlem103  46788  fourierdlem104  46789  fouriersw  46810  etransclem37  46850  sge0splitmpt  46990  sge0xaddlem2  47013  sge0xadd  47014  caragen0  47085  caragenuncllem  47091  nthrucw  47467  goldrasin  47481  goldratmolem2  47485  fsumsplitsndif  47980  139prmALT  48210  127prm  48213  m11nprm  48215  3exp4mod41  48230  ppivalnn4  48241  sbgoldbo  48414  2t6m3t4e0  48975  lincsum  49056  zlmodzxzequa  49123  zlmodzxzequap  49126  zlmodzxzldeplem3  49129  rrx2linest  49369  line2  49379  itsclc0yqsollem1  49389  itsclquadb  49403  itscnhlinecirc02plem2  49410  postcofval  49990  postcofcl  49991  precofval  49993  precofvalALT  49994  precofcl  49996  termcfuncval  50158