MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim2i Unicode version

Theorem anim2i 554
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1
Assertion
Ref Expression
anim2i

Proof of Theorem anim2i
StepHypRef Expression
1 id 21 . 2
2 anim1i.1 . 2
31, 2anim12i 551 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360
This theorem is referenced by:  sylanl2  634  sylanr2  636  andi  839  thema1a  1557  sbimi  1683  19.41OLD  1905  exdistrf  2074  exdistrfOLD  2075  equs45f  2096  moaneu  2389  eupickbOLD  2397  2eu1  2414  darii  2433  festino  2439  baroco  2440  r19.27av  2898  rspc2ev  3121  reu3  3187  difrab  3660  trssord  4757  ordnbtwn  4831  imainss  5274  fof  5637  f1ocnv  5670  fv3  5720  fvelimab  5763  dff2  5871  dffo5  5876  fnsnb  5913  dff1o6  5994  oprabid  6127  ssoprab2i  6191  ndmovass  6261  ndmovdistr  6262  tfi  6474  find  6511  releldm2  6630  bropopvvv  6659  tfrlem5  6803  omlimcl  6983  odi  6984  ixpf  7248  infcntss  7546  hartogs  7680  card2on  7689  epfrs  7834  acni3  8099  dfac2  8182  cflm  8301  axdc2lem  8499  ac6s  8535  ondomon  8609  axregndlem1  8648  axregnd  8650  eltsk2g  8797  grothpw  8872  grothpwex  8873  grothomex  8875  ltexprlem1  9084  ltexprlem4  9087  recexsrlem  9149  lediv2a  10092  lbreu  10146  elfzp12  11391  dfceil2  11529  ccatsymb  12128  swrdccatin2  12225  swrdccatin12lem2  12227  swrdccatin12  12229  repswsymball  12264  cshwidxmod  12287  repswcshw  12293  cau3lem  12689  rlimres  12883  dvdsnegb  13397  dvds2add  13411  dvds2sub  13412  ndvdssub  13458  cshwshashlem2  13970  isfunc  14615  drsdirfi  14949  gimcnv  15625  gaid  15647  symg2bas  15684  lmhmlem  16724  lmimcnv  16762  abvn0b  16987  prmirredlem  17398  psgndiflemB  17698  matbas2  17792  tposmap  17812  1marepvsma1  17862  maducoeval2  17920  smadiadetlem3lem0  17945  slesolinv  17960  cramerimplem1  17963  cramerimplem2  17964  toponcom  18009  neitr  18258  cnprest  18367  nrmsep2  18434  bwth  18487  2ndcsep  18537  reghaus  18872  isfil2  18903  alexsubALTlem3  19095  cnextcn  19113  lpbl  19548  iscau4  20247  caussi  20265  cmetcuspOLD  20322  cmetcusp  20323  ovolicc2lem3  20430  limcresi  20787  elply2  21130  elqaa  21254  aannenlem1  21260  aannenlem2  21261  bpos1lem  22087  uhgrares  22364  usgrares  22410  usgraexmpl  22441  cusgra3v  22494  cusgrafilem2  22510  redwlk  22627  wlkdvspthlem  22628  cyclispthon  22641  usgrcyclnl1  22648  3v3e3cycl1  22652  eupatrl  22711  isgrpo  22805  gxsub  22885  rngmgmbs4  23026  vcz  23070  sspival  23258  hvsub4  23561  hvaddsub4  23602  5oalem2  24180  5oalem5  24183  5oalem6  24184  3oalem2  24188  homcl  24272  hoadddi  24329  stle0i  24765  spansncv2  24819  mdsymlem1  24929  cdj3lem1  24960  spc2ed  24984  disjin  25057  gsumle  25406  gsumvsca1  25412  gsumvsca2  25413  sxbrsigalem0  25866  dya2icoseg2  25873  eulerpartlemgvv  25933  ballotlemirc  26064  axcont  27254  colineardim1  27334  idinside  27357  lukshef-ax2  27504  ovoliunnfl  27613  itg2addnclem  27623  finminlem  27693  ivthALT  27710  indexa  27807  sstotbnd3  27857  heibor1lem  27890  heibor1  27891  eldioph4i  28299  acongtr  28469  aaitgo  28707  dvsconst  28778  stoweidlem17  28991  dmfcoafv  29260  f13dfv  29328  elfzelfzlble  29388  powm2modprm  29429  wwlktovfo  29434  wwlknimp  29502  wlkiswwlkfun  29530  wlkiswwlkinj  29531  wwlknred  29536  wwlknextbi  29538  wwlknfi  29551  2wlkonotv  29577  clwwlknprop  29616  wwlkext2clwwlk  29646  clwwnisshclwwn  29654  eleclclwwlknlem1  29671  clwlkfoclwwlk  29699  clwlknclwlkdifs  29759  frgraunss  29768  frgranbnb  29793  frgrawopreg  29823  frg2woteq  29834  numclwlk3lem3  29847  numclwwlkffin  29856  numclwwlkovf2ex  29860  numclwwlk1  29872  numclwwlkqhash  29874  numclwwlk2lem1  29876  numclwlk2lem2f  29877  numclwwlk5  29886  numclwwlk7  29888  frgraregord013  29892  bnj145OLD  30564  bnj168  30567  bnj546  30737  bnj594  30753  bnj1097  30820  bnj1110  30821  bnj1174  30842  bnj1176  30844  axc9lem2wAUX11  31008  exdistrfNEW11  31057  equs45fNEW11  31172  axc9lem2OLD11  31257  dalem53  32072  dalem54  32073  linepsubN  32099  pmapsub  32115  elpaddri  32149  pclfinN  32247  pclcmpatN  32248  cdlemg33c0  33049  dihatexv2  33687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator