MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq12i Structured version   Visualization version   GIF version

Theorem oveq12i 6702
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
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq12i.2 . 2 𝐶 = 𝐷
3 oveq12 6699 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 708 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  oveq123i  6704  caovdir  6910  caovdilem  6911  caovlem2  6912  cnfcom2  8637  canthwelem  9510  adderpqlem  9814  addassnq  9818  distrnq  9821  ltanq  9831  1lt2nq  9833  ltexnq  9835  halfnq  9836  mulcmpblnrlem  9929  mulcomsr  9948  distrsr  9950  m1p1sr  9951  m1m1sr  9952  mulgt0sr  9964  addcnsrec  10002  mulcnsrec  10003  axmulcom  10014  axmulass  10016  axdistr  10017  axi2m1  10018  addid1  10254  3t3e9  11218  8th4div3  11290  halfpm6th  11291  numma  11595  decmul10add  11631  decmul10addOLD  11632  4t3lem  11669  9t11e99  11709  9t11e99OLD  11710  halfthird  11723  5recm6rec  11724  fz0to3un2pr  12480  seqfeq4  12890  seqof  12898  sqdivi  12988  sq4e2t8  13002  i4  13007  binom2i  13014  nn0opthlem1  13095  facp1  13105  fac2  13106  fac3  13107  fac4  13108  faclbnd4lem1  13120  4bc2eq6  13156  ccat2s1len  13442  ccat2s1p2  13450  cats1len  13651  cats2cat  13653  ofs2  13756  cji  13943  sqrlem5  14031  fsumadd  14514  fsumsplitf  14516  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  0.999...  14656  0.999...OLD  14657  fprodmul  14734  fproddiv  14735  fprodsplitf  14763  bpoly3  14833  fsumcube  14835  efsep  14884  ef01bndlem  14958  cos2bnd  14962  rpnnen2lem3  14989  3dvds2dec  15103  3dvds2decOLD  15104  flodddiv4  15184  sadeq  15241  gcdaddmlem  15292  bezout  15307  nn0gcdsq  15507  pythagtriplem16  15582  4sqlem19  15714  dec5nprm  15817  dec2nprm  15818  mod2xnegi  15822  numexp2x  15830  decsplit  15834  decsplitOLD  15838  karatsuba  15839  karatsubaOLD  15840  2exp16  15844  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  funcoppc  16582  estrchom  16814  funcestrcsetclem5  16831  yonedalem3b  16966  gsum2dlem2  18416  opprring  18677  isrhm  18769  evlsval  19567  mamudi  20257  mamudir  20258  oftpos  20306  mamutpos  20312  mdetrlin  20456  mdetrlin2  20461  mdetunilem5  20470  cpmadugsumfi  20730  cnmpt2res  21528  ussval  22110  icopnfhmeo  22789  iccpnfhmeo  22791  pcoass  22870  ovolunlem1a  23310  ioombl1lem3  23374  ioombl1lem4  23375  mbfimaopnlem  23467  iblcnlem1  23599  itgfsum  23638  iblabslem  23639  itgsplit  23647  dveflem  23787  efhalfpi  24268  efipi  24270  sin2pi  24272  ef2pi  24274  sincosq3sgn  24297  sincosq4sgn  24298  sinq34lt0t  24306  sincos4thpi  24310  tan4thpi  24311  sincos6thpi  24312  sincos3rdpi  24313  pige3  24314  cxpcn3  24534  lawcos  24591  1cubrlem  24613  quart1lem  24627  quart1  24628  asin1  24666  atancj  24682  atanlogsublem  24687  log2cnv  24716  log2tlbnd  24717  log2ublem3  24720  log2ub  24721  birthday  24726  basellem8  24859  basellem9  24860  cht2  24943  cht3  24944  1sgm2ppw  24970  bclbnd  25050  bposlem8  25061  bposlem9  25062  lgsdi  25104  lgsquadlem1  25150  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  mirauto  25624  axsegconlem9  25850  ax5seglem7  25860  vtxdginducedm1  26495  clwlksfoclwwlk  27050  eupth2eucrct  27195  ex-exp  27437  ex-fac  27438  ex-bc  27439  ex-hash  27440  ip0i  27808  ip1ilem  27809  ip2i  27811  ipdirilem  27812  ipasslem10  27822  ip2dii  27827  pythi  27833  siilem1  27834  hvsubsub4i  28044  hvsubcan2i  28049  hisubcomi  28089  normlem0  28094  normlem1  28095  normlem2  28096  normlem3  28097  normlem6  28100  normlem8  28102  normlem9  28103  bcseqi  28105  norm-ii-i  28122  norm-iii-i  28124  normpythi  28127  norm3difi  28132  normpari  28139  normpar2i  28141  polid2i  28142  polidi  28143  bcsiALT  28164  lediri  28524  h1de2i  28540  cmcmlem  28578  cmbr2i  28583  cm2j  28607  fh3i  28610  fh4i  28611  pjaddii  28662  pjsslem  28666  pjssmii  28668  pjdifnormii  28670  lnopeq0lem1  28992  lnopunilem1  28997  lnophmlem2  29004  pjsdi2i  29144  pjclem1  29182  golem1  29258  dpmul100  29733  dpmul1000  29735  dpadd2  29746  dpadd  29747  dpadd3  29748  dpmul  29749  dpmul4  29750  gsumle  29907  rmulccn  30102  raddcn  30103  xrmulc1cn  30104  xrge0iifhmeo  30110  qqh0  30156  qqh1  30157  elmbfmvol2  30457  mbfmcnt  30458  eulerpartlemgvv  30566  eulerpartlemgh  30568  fib2  30592  fib3  30593  fib4  30594  fib5  30595  fib6  30596  ballotlem2  30678  ballotlemfval0  30685  ballotth  30727  hgt750lem2  30858  problem2  31685  problem2OLD  31686  problem4  31688  quad3  31690  pigt3  33532  poimirlem30  33569  iblabsnclem  33603  dalem10  35277  cdleme0e  35822  cdleme7c  35850  cdleme20c  35916  mzpcompact2lem  37631  pellexlem5  37714  pellfundgt1  37764  jm2.27c  37891  areaquad  38119  lhe4.4ex1a  38845  mccl  40148  dvnprodlem2  40480  itgsin0pilem1  40483  stoweidlem13  40548  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  dirkerper  40631  dirkertrigeqlem1  40633  fourierdlem30  40672  fourierdlem47  40688  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  etransclem37  40806  sge0splitmpt  40946  sge0xaddlem2  40969  sge0xadd  40970  caragen0  41041  caragenuncllem  41047  fsumsplitsndif  41668  2exp5  41832  139prmALT  41836  127prm  41840  2exp11  41842  m11nprm  41843  3exp4mod41  41858  sbgoldbo  42000  2t6m3t4e0  42451  lincsum  42543  zlmodzxzequa  42610  zlmodzxzequap  42613  zlmodzxzldeplem3  42616
  Copyright terms: Public domain W3C validator