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

Theorem oveq12i 7151
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 7148 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 691 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7139
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142
This theorem is referenced by:  oveq123i  7153  caovdir  7366  caovdilem  7367  caovlem2  7368  cnfcom2  9153  canthwelem  10065  adderpqlem  10369  addassnq  10373  distrnq  10376  ltanq  10386  1lt2nq  10388  ltexnq  10390  halfnq  10391  mulcmpblnrlem  10485  mulcomsr  10504  distrsr  10506  m1p1sr  10507  m1m1sr  10508  mulgt0sr  10520  addcnsrec  10558  mulcnsrec  10559  axmulcom  10570  axmulass  10572  axdistr  10573  axi2m1  10574  addid1  10813  3t3e9  11796  8th4div3  11849  halfpm6th  11850  numma  12134  decmul10add  12159  4t3lem  12187  9t11e99  12220  halfthird  12233  5recm6rec  12234  fz0to3un2pr  13008  seqfeq4  13419  seqof  13427  sqdivi  13548  sq4e2t8  13562  i4  13567  binom2i  13574  nn0opthlem1  13628  facp1  13638  fac2  13639  fac3  13640  fac4  13641  faclbnd4lem1  13653  4bc2eq6  13689  ccat2s1len  13972  ccat2s1lenOLD  13973  ccat2s1p2  13981  ccat2s1p2OLD  13983  cats1len  14217  cats2cat  14219  ofs2  14326  cji  14514  sqrlem5  14602  fsumadd  15092  fsumsplitf  15094  fsumsplitsnun  15106  0.999...  15233  fprodmul  15310  fproddiv  15311  fprodsplitf  15338  bpoly3  15408  fsumcube  15410  efsep  15459  ef01bndlem  15533  cos2bnd  15537  rpnnen2lem3  15565  3dvds2dec  15678  flodddiv4  15758  sadeq  15815  gcdaddmlem  15866  bezout  15885  nn0gcdsq  16086  pythagtriplem16  16161  4sqlem19  16293  dec5nprm  16396  dec2nprm  16397  mod2xnegi  16401  numexp2x  16409  decsplit  16413  karatsuba  16414  2exp5  16416  2exp16  16420  37prm  16450  43prm  16451  83prm  16452  139prm  16453  163prm  16454  317prm  16455  631prm  16456  1259lem1  16460  1259lem2  16461  1259lem3  16462  1259lem4  16463  1259lem5  16464  1259prm  16465  2503lem1  16466  2503lem2  16467  2503lem3  16468  2503prm  16469  4001lem1  16470  4001lem2  16471  4001lem3  16472  4001lem4  16473  4001prm  16474  funcoppc  17141  estrchom  17373  funcestrcsetclem5  17390  yonedalem3b  17525  symgressbas  18506  gsum2dlem2  19088  opprring  19381  isrhm  19473  evlsval  20762  mamudi  21012  mamudir  21013  oftpos  21061  mamutpos  21067  mdetrlin  21211  mdetrlin2  21216  mdetunilem5  21225  cpmadugsumfi  21486  cnmpt2res  22286  ussval  22869  icopnfhmeo  23552  iccpnfhmeo  23554  pcoass  23633  ovolunlem1a  24104  ioombl1lem3  24168  ioombl1lem4  24169  mbfimaopnlem  24263  itgfsum  24434  iblabslem  24435  itgsplit  24443  dveflem  24586  efhalfpi  25068  efipi  25070  sin2pi  25072  ef2pi  25074  sincosq3sgn  25097  sincosq4sgn  25098  sinq34lt0t  25106  sincos4thpi  25110  tan4thpi  25111  sincos6thpi  25112  sincos3rdpi  25113  pigt3  25114  pige3ALT  25116  cxpcn3  25341  lawcos  25406  1cubrlem  25431  quart1lem  25445  quart1  25446  asin1  25484  atancj  25500  atanlogsublem  25505  log2cnv  25534  log2tlbnd  25535  log2ublem3  25538  log2ub  25539  birthday  25544  basellem8  25677  basellem9  25678  cht2  25761  cht3  25762  1sgm2ppw  25788  bclbnd  25868  bposlem8  25879  bposlem9  25880  lgsdi  25922  lgsquadlem1  25968  2lgsoddprmlem3c  26000  2lgsoddprmlem3d  26001  addsqnreup  26031  mirauto  26482  axsegconlem9  26723  ax5seglem7  26733  vtxdginducedm1  27337  clwlkclwwlkfo  27798  eupth2eucrct  28006  ex-exp  28239  ex-fac  28240  ex-bc  28241  ex-hash  28242  ip0i  28612  ip1ilem  28613  ip2i  28615  ipdirilem  28616  ipasslem10  28626  ip2dii  28631  pythi  28637  siilem1  28638  hvsubsub4i  28846  hvsubcan2i  28851  hisubcomi  28891  normlem0  28896  normlem1  28897  normlem2  28898  normlem3  28899  normlem6  28902  normlem8  28904  normlem9  28905  bcseqi  28907  norm-ii-i  28924  norm-iii-i  28926  normpythi  28929  norm3difi  28934  normpari  28941  normpar2i  28943  polid2i  28944  polidi  28945  bcsiALT  28966  lediri  29324  h1de2i  29340  cmcmlem  29378  cmbr2i  29383  cm2j  29407  fh3i  29410  fh4i  29411  pjaddii  29462  pjsslem  29466  pjssmii  29468  pjdifnormii  29470  lnopeq0lem1  29792  lnopunilem1  29797  lnophmlem2  29804  pjsdi2i  29944  pjclem1  29982  golem1  30058  dpmul100  30603  dpmul1000  30605  dpadd2  30616  dpadd  30617  dpadd3  30618  dpmul  30619  dpmul4  30620  gsumle  30779  matdim  31105  rmulccn  31285  raddcn  31286  xrmulc1cn  31287  xrge0iifhmeo  31293  qqh0  31339  qqh1  31340  elmbfmvol2  31639  mbfmcnt  31640  eulerpartlemgvv  31748  eulerpartlemgh  31750  fib2  31774  fib3  31775  fib4  31776  fib5  31777  fib6  31778  ballotlem2  31860  ballotlemfval0  31867  ballotth  31909  hgt750lem2  32037  problem2  33023  problem4  33025  quad3  33027  poimirlem30  35086  iblabsnclem  35119  dalem10  36968  cdleme0e  37512  cdleme7c  37540  cdleme20c  37606  5bc2eq10  39343  sn-1ne2  39459  sqmid3api  39470  sqdeccom12  39476  sq3deccom12  39477  nn0expgcd  39485  rei4  39553  ipiiie0  39567  sn-0tie0  39569  sn-0lt1  39580  mzpcompact2lem  39685  pellexlem5  39767  pellfundgt1  39817  jm2.27c  39941  areaquad  40159  resqrtvalex  40338  imsqrtvalex  40339  lhe4.4ex1a  41026  mccl  42233  dvnprodlem2  42582  itgsin0pilem1  42585  stoweidlem13  42648  wallispilem4  42703  wallispi2lem1  42706  wallispi2lem2  42707  dirkerper  42731  dirkertrigeqlem1  42733  fourierdlem30  42772  fourierdlem47  42788  fourierdlem103  42844  fourierdlem104  42845  fouriersw  42866  etransclem37  42906  sge0splitmpt  43043  sge0xaddlem2  43066  sge0xadd  43067  caragen0  43138  caragenuncllem  43144  fsumsplitsndif  43883  139prmALT  44106  127prm  44109  2exp11  44111  m11nprm  44112  3exp4mod41  44127  sbgoldbo  44298  2t6m3t4e0  44743  lincsum  44831  zlmodzxzequa  44898  zlmodzxzequap  44901  zlmodzxzldeplem3  44904  rrx2linest  45149  line2  45159  itsclc0yqsollem1  45169  itsclquadb  45183  itscnhlinecirc02plem2  45190
  Copyright terms: Public domain W3C validator