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

Theorem anim2i 553
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 20 . 2  |-  ( ch 
->  ch )
2 anim1i.1 . 2  |-  ( ph  ->  ps )
31, 2anim12i 550 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylanl2  633  sylanr2  635  andi  838  sbimi  1660  19.41OLD  1897  exdistrf  2028  equs45f  2044  eupickb  2319  2eu1  2334  darii  2353  festino  2359  baroco  2360  r19.27av  2804  rspc2ev  3020  reu3  3084  difrab  3575  trssord  4558  ordnbtwn  4631  tfi  4792  find  4829  imainss  5246  fof  5612  f1ocnv  5646  fv3  5703  fvelimab  5741  dff2  5840  dffo5  5845  dff1o6  5972  oprabid  6064  ssoprab2i  6121  ndmovass  6194  ndmovdistr  6195  releldm2  6356  bropopvvv  6385  tfrlem5  6600  omlimcl  6780  odi  6781  ixpf  7043  infcntss  7339  hartogs  7469  card2on  7478  epfrs  7623  acni3  7884  dfac2  7967  cflm  8086  axdc2lem  8284  ac6s  8320  ondomon  8394  axregndlem1  8433  axregnd  8435  eltsk2g  8582  grothpw  8657  grothpwex  8658  grothomex  8660  ltexprlem1  8869  ltexprlem4  8872  recexsrlem  8934  lediv2a  9860  lbreu  9914  elfzp12  11081  cau3lem  12113  rlimres  12307  dvdsnegb  12822  dvds2add  12836  dvds2sub  12837  ndvdssub  12882  isfunc  14016  drsdirfi  14350  spweu  14614  gimcnv  15009  gaid  15031  lmhmlem  16060  lmimcnv  16094  abvn0b  16317  prmirredlem  16728  toponcom  16950  neitr  17198  cnprest  17307  nrmsep2  17374  2ndcsep  17475  reghaus  17810  isfil2  17841  alexsubALTlem3  18033  cnextcn  18051  lpbl  18486  iscau4  19185  caussi  19203  cmetcuspOLD  19260  cmetcusp  19261  ovolicc2lem3  19368  limcresi  19725  elply2  20068  elqaa  20192  aannenlem1  20198  aannenlem2  20199  bpos1lem  21019  uhgrares  21296  usgrares  21342  usgraexmpl  21373  cusgra3v  21426  cusgrafilem2  21442  redwlk  21559  wlkdvspthlem  21560  cyclispthon  21573  usgrcyclnl1  21580  3v3e3cycl1  21584  eupatrl  21643  isgrpo  21737  gxsub  21817  rngmgmbs4  21958  vcz  22002  sspival  22190  hvsub4  22492  hvaddsub4  22533  5oalem2  23110  5oalem5  23113  5oalem6  23114  3oalem2  23118  homcl  23202  hoadddi  23259  stle0i  23695  spansncv2  23749  mdsymlem1  23859  cdj3lem1  23890  disjin  23980  sxbrsigalem0  24574  dya2icoseg2  24581  ballotlemirc  24742  axcont  25819  colineardim1  25899  idinside  25922  lukshef-ax2  26069  ovoliunnfl  26147  itg2addnclem  26155  finminlem  26211  ivthALT  26228  indexa  26325  sstotbnd3  26375  heibor1lem  26408  heibor1  26409  eldioph4i  26763  acongtr  26933  aaitgo  27235  dvsconst  27415  stoweidlem17  27633  dmfcoafv  27906  f13dfv  27962  swrdccatin12lem3  28024  swrdccatin12  28026  2wlkonotv  28074  frgraunss  28099  frgranbnb  28124  frgrawopreg  28152  frg2woteq  28163  bnj145  28800  bnj168  28803  bnj546  28973  bnj594  28989  bnj1097  29056  bnj1110  29057  bnj1174  29078  bnj1176  29080  ax12olem2wAUX7  29162  exdistrfNEW7  29211  equs45fNEW7  29322  ax12olem2OLD7  29390  dalem53  30207  dalem54  30208  linepsubN  30234  pmapsub  30250  elpaddri  30284  pclfinN  30382  pclcmpatN  30383  cdlemg33c0  31184  dihatexv2  31822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator