Theorem oveq12i 7425

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

Syntax hints:   = wceq 1567  (class class class)co 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6495  df-fv 6547  df-ov 7416

This theorem is referenced by:  oveq123i  7427  caovdir  7647  caovdilem  7648  caovlem2  7649  cnfcom2  9673  canthwelem  10637  adderpqlem  10941  addassnq  10945  distrnq  10948  ltanq  10958  1lt2nq  10960  ltexnq  10962  halfnq  10963  mulcmpblnrlem  11057  mulcomsr  11076  distrsr  11078  m1p1sr  11079  m1m1sr  11080  mulgt0sr  11092  addcnsrec  11130  mulcnsrec  11131  axmulcom  11142  axmulass  11144  axdistr  11145  axi2m1  11146  addrid  11392  3t3e9  12410  8th4div3  12466  halfthird  12467  numma  12762  decmul10add  12787  4t3lem  12815  9t11e99OLD  12849  5recm6rec  12863  fz0to3un2pr  13659  seqfeq4  14089  seqof  14097  sqdivi  14223  sq4e2t8  14237  i4  14242  binom2i  14250  nn0opthlem1  14306  facp1  14316  fac2  14317  fac3  14318  fac4  14319  faclbnd4lem1  14331  4bc2eq6  14367  ccat2s1len  14663  ccat2s1p2  14670  cats1len  14899  cats2cat  14901  ofs2  15010  cji  15212  01sqrexlem5  15299  fsumadd  15793  fsumsplitf  15795  fsumsplitsnun  15808  0.999...  15937  fprodmul  16016  fproddiv  16017  fprodsplitf  16044  bpoly3  16114  fsumcube  16116  efsep  16168  ef01bndlem  16242  cos2bnd  16246  rpnnen2lem3  16274  3dvds2dec  16393  flodddiv4  16475  sadeq  16532  gcdaddmlem  16584  bezout  16603  nn0expgcd  16624  nn0gcdsq  16813  pythagtriplem16  16892  4sqlem19  17025  dec5nprm  17128  dec2nprm  17129  mod2xnegi  17133  numexp2x  17140  decsplit  17144  karatsuba  17145  2exp5  17147  2exp11  17151  2exp16  17152  37prm  17183  43prm  17184  83prm  17185  139prm  17186  163prm  17187  317prm  17188  631prm  17189  1259lem1  17193  1259lem2  17194  1259lem3  17195  1259lem4  17196  1259lem5  17197  1259prm  17198  2503lem1  17199  2503lem2  17200  2503lem3  17201  2503prm  17202  4001lem1  17203  4001lem2  17204  4001lem3  17205  4001lem4  17206  4001prm  17207  funcoppc  17934  estrchom  18185  funcestrcsetclem5  18202  yonedalem3b  18337  ecqusaddd  19265  symgressbas  19454  gsum2dlem2  20043  gsumle  20217  opprrng  20429  isrhm  20562  rngqiprnglinlem2  21405  pzriprng1ALT  21617  evlsval  22208  mamudi  22531  mamudir  22532  oftpos  22580  mamutpos  22586  mdetrlin  22730  mdetrlin2  22735  mdetunilem5  22744  cpmadugsumfi  23005  cnmpt2res  23805  ussval  24387  icopnfhmeo  25073  iccpnfhmeo  25075  pcoass  25154  ovolunlem1a  25626  ioombl1lem3  25690  ioombl1lem4  25691  mbfimaopnlem  25785  itgfsum  25957  iblabslem  25958  itgsplit  25966  dveflem  26109  efhalfpi  26604  efipi  26606  sin2pi  26608  ef2pi  26610  sincosq3sgn  26633  sincosq4sgn  26634  sinq34lt0t  26642  sincos4thpi  26646  tan4thpi  26647  tan4thpiOLD  26648  sincos6thpi  26649  sincos3rdpi  26650  pigt3  26651  pige3ALT  26653  cxpcn3  26881  lawcos  26949  1cubrlem  26974  quart1lem  26988  quart1  26989  asin1  27027  atancj  27043  atanlogsublem  27048  log2cnv  27077  log2tlbnd  27078  log2ublem3  27081  log2ub  27082  birthday  27087  basellem8  27220  basellem9  27221  cht2  27304  cht3  27305  1sgm2ppw  27332  bclbnd  27412  bposlem8  27423  bposlem9  27424  lgsdi  27466  lgsquadlem1  27512  2lgsoddprmlem3c  27544  2lgsoddprmlem3d  27545  addsqnreup  27575  addsval2  28124  addsunif  28163  addsasslem1  28164  addsasslem2  28165  negsval  28186  neg0s  28187  neg1s  28188  negsid  28202  mulsval2  28272  muls01  28273  mulsproplem2  28278  mulsproplem3  28279  mulsproplem4  28280  mulsproplem5  28281  mulsproplem6  28282  mulsproplem7  28283  mulsproplem8  28284  mulsproplem12  28288  mulsproplem13  28289  mulsproplem14  28290  mulsunif  28311  addsdilem1  28312  addsdilem2  28313  mulsasslem1  28324  mulsasslem2  28325  mulsunif2  28331  precsexlem11  28378  onmulscl  28439  twocut  28584  mirauto  28925  axsegconlem9  29218  ax5seglem7  29228  vtxdginducedm1  29836  clwlkclwwlkfo  30303  eupth2eucrct  30511  ex-exp  30744  ex-fac  30745  ex-bc  30746  ex-hash  30747  ip0i  31120  ip1ilem  31121  ip2i  31123  ipdirilem  31124  ipasslem10  31134  ip2dii  31139  pythi  31145  siilem1  31146  hvsubsub4i  31354  hvsubcan2i  31359  hisubcomi  31399  normlem0  31404  normlem1  31405  normlem2  31406  normlem3  31407  normlem6  31410  normlem8  31412  normlem9  31413  bcseqi  31415  norm-ii-i  31432  norm-iii-i  31434  normpythi  31437  norm3difi  31442  normpari  31449  normpar2i  31451  polid2i  31452  polidi  31453  bcsiALT  31474  lediri  31832  h1de2i  31848  cmcmlem  31886  cmbr2i  31891  cm2j  31915  fh3i  31918  fh4i  31919  pjaddii  31970  pjsslem  31974  pjssmii  31976  pjdifnormii  31978  lnopeq0lem1  32300  lnopunilem1  32305  lnophmlem2  32312  pjsdi2i  32452  pjclem1  32490  golem1  32566  dpmul100  33159  dpmul1000  33161  dpadd2  33172  dpadd  33173  dpadd3  33174  dpmul  33175  dpmul4  33176  ccatws1f1o  33214  elrgspnlem2  33506  matdim  33952  fldext2chn  34065  constrextdg2lem  34085  constrext2chnlem  34087  iconstr  34103  cos9thpiminplylem4  34122  cos9thpiminplylem5  34123  rmulccn  34265  raddcn  34266  xrmulc1cn  34267  xrge0iifhmeo  34273  qqh0  34321  qqh1  34322  elmbfmvol2  34604  mbfmcnt  34605  eulerpartlemgvv  34713  eulerpartlemgh  34715  fib2  34739  fib3  34740  fib4  34741  fib5  34742  fib6  34743  ballotlem2  34826  ballotlemfval0  34833  ballotth  34875  hgt750lem2  34986  problem2  36093  problem4  36095  quad3  36097  ditgeq123i  36646  cbvditgvw2  36686  poimirlem30  38226  iblabsnclem  38259  dalem10  40374  cdleme0e  40918  cdleme7c  40946  cdleme20c  41012  3exp7  42747  3lexlogpow5ineq1  42748  3lexlogpow5ineq5  42754  aks4d1p1  42770  5bc2eq10  42836  aks5lem3a  42883  25or6to4  42900  sn-1ne2  42959  sqmid3api  42971  sqdeccom12  42977  sq3deccom12  42978  tan3rdpi  43040  sin2t3rdpi  43041  cos2t3rdpi  43042  rei4  43112  ipiiie0  43126  sn-0tie0  43152  mzpcompact2lem  43411  pellexlem5  43489  pellfundgt1  43539  jm2.27c  43663  areaquad  43872  resqrtvalex  44300  imsqrtvalex  44301  lhe4.4ex1a  44968  mccl  46243  dvnprodlem2  46590  itgsin0pilem1  46593  stoweidlem13  46656  wallispilem4  46711  wallispi2lem1  46714  wallispi2lem2  46715  dirkerper  46739  dirkertrigeqlem1  46741  fourierdlem30  46780  fourierdlem47  46796  fourierdlem103  46852  fourierdlem104  46853  fouriersw  46874  etransclem37  46914  sge0splitmpt  47054  sge0xaddlem2  47077  sge0xadd  47078  caragen0  47149  caragenuncllem  47155  nthrucw  47531  goldrasin  47545  goldratmolem2  47549  fsumsplitsndif  48044  139prmALT  48274  127prm  48277  m11nprm  48279  3exp4mod41  48294  ppivalnn4  48305  sbgoldbo  48478  2t6m3t4e0  49050  lincsum  49131  zlmodzxzequa  49198  zlmodzxzequap  49201  zlmodzxzldeplem3  49204  rrx2linest  49444  line2  49454  itsclc0yqsollem1  49464  itsclquadb  49478  itscnhlinecirc02plem2  49485  postcofval  50064  postcofcl  50065  precofval  50067  precofvalALT  50068  precofcl  50070  termcfuncval  50232