MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim2i Structured version   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  |-  ( ph  ->  ps )
Assertion
Ref Expression
anim2i  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )

Proof of Theorem anim2i
StepHypRef Expression
1 id 21 . 2  |-  ( ch 
->  ch )
2 anim1i.1 . 2  |-  ( ph  ->  ps )
31, 2anim12i 551 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  sylanl2  634  sylanr2  636  andi  839  sbimi  1665  19.41OLD  1902  exdistrf  2067  exdistrfOLD  2068  equs45f  2089  eupickb  2348  2eu1  2363  darii  2382  festino  2388  baroco  2389  r19.27av  2846  rspc2ev  3062  reu3  3126  difrab  3617  trssord  4601  ordnbtwn  4675  tfi  4836  find  4873  imainss  5290  fof  5656  f1ocnv  5690  fv3  5747  fvelimab  5785  dff2  5884  dffo5  5889  dff1o6  6016  oprabid  6108  ssoprab2i  6165  ndmovass  6238  ndmovdistr  6239  releldm2  6400  bropopvvv  6429  tfrlem5  6644  omlimcl  6824  odi  6825  ixpf  7087  infcntss  7383  hartogs  7516  card2on  7525  epfrs  7670  acni3  7933  dfac2  8016  cflm  8135  axdc2lem  8333  ac6s  8369  ondomon  8443  axregndlem1  8482  axregnd  8484  eltsk2g  8631  grothpw  8706  grothpwex  8707  grothomex  8709  ltexprlem1  8918  ltexprlem4  8921  recexsrlem  8983  lediv2a  9909  lbreu  9963  elfzp12  11131  cau3lem  12163  rlimres  12357  dvdsnegb  12872  dvds2add  12886  dvds2sub  12887  ndvdssub  12932  isfunc  14066  drsdirfi  14400  spweu  14664  gimcnv  15059  gaid  15081  lmhmlem  16110  lmimcnv  16144  abvn0b  16367  prmirredlem  16778  toponcom  17000  neitr  17249  cnprest  17358  nrmsep2  17425  2ndcsep  17527  reghaus  17862  isfil2  17893  alexsubALTlem3  18085  cnextcn  18103  lpbl  18538  iscau4  19237  caussi  19255  cmetcuspOLD  19312  cmetcusp  19313  ovolicc2lem3  19420  limcresi  19777  elply2  20120  elqaa  20244  aannenlem1  20250  aannenlem2  20251  bpos1lem  21071  uhgrares  21348  usgrares  21394  usgraexmpl  21425  cusgra3v  21478  cusgrafilem2  21494  redwlk  21611  wlkdvspthlem  21612  cyclispthon  21625  usgrcyclnl1  21632  3v3e3cycl1  21636  eupatrl  21695  isgrpo  21789  gxsub  21869  rngmgmbs4  22010  vcz  22054  sspival  22242  hvsub4  22544  hvaddsub4  22585  5oalem2  23162  5oalem5  23165  5oalem6  23166  3oalem2  23170  homcl  23254  hoadddi  23311  stle0i  23747  spansncv2  23801  mdsymlem1  23911  cdj3lem1  23942  disjin  24032  sxbrsigalem0  24626  dya2icoseg2  24633  ballotlemirc  24794  axcont  25920  colineardim1  26000  idinside  26023  lukshef-ax2  26170  ovoliunnfl  26260  itg2addnclem  26270  finminlem  26335  ivthALT  26352  indexa  26449  sstotbnd3  26499  heibor1lem  26532  heibor1  26533  eldioph4i  26887  acongtr  27057  aaitgo  27358  dvsconst  27538  stoweidlem17  27756  dmfcoafv  28029  f13dfv  28099  swrdccatin2  28244  swrdccatin12lem3  28246  swrdccatin12  28248  cshwidx  28276  cshwidxm1  28279  cshwidxm  28280  cshwidxn  28281  2cshw2lem1  28286  cshwssizelem2  28315  cshwssizelem4a  28317  wwlknimp  28369  2wlkonotv  28409  frgraunss  28459  frgranbnb  28484  frgrawopreg  28512  frg2woteq  28523  bnj145  29168  bnj168  29171  bnj546  29341  bnj594  29357  bnj1097  29424  bnj1110  29425  bnj1174  29446  bnj1176  29448  ax12olem2wAUX7  29530  exdistrfNEW7  29579  equs45fNEW7  29695  ax12olem2OLD7  29780  dalem53  30596  dalem54  30597  linepsubN  30623  pmapsub  30639  elpaddri  30673  pclfinN  30771  pclcmpatN  30772  cdlemg33c0  31573  dihatexv2  32211
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