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  1659  19.41OLD  1890  exdistrf  2012  equs45f  2026  eupickb  2304  2eu1  2319  darii  2338  festino  2344  baroco  2345  r19.27av  2788  rspc2ev  3004  reu3  3068  difrab  3559  trssord  4540  ordnbtwn  4613  tfi  4774  find  4811  imainss  5228  fof  5594  f1ocnv  5628  fv3  5685  fvelimab  5722  dff2  5821  dffo5  5826  dff1o6  5953  oprabid  6045  ssoprab2i  6102  ndmovass  6175  ndmovdistr  6176  releldm2  6337  bropopvvv  6366  tfrlem5  6578  omlimcl  6758  odi  6759  ixpf  7021  infcntss  7317  hartogs  7447  card2on  7456  epfrs  7601  acni3  7862  dfac2  7945  cflm  8064  axdc2lem  8262  ac6s  8298  ondomon  8372  axregndlem1  8411  axregnd  8413  eltsk2g  8560  grothpw  8635  grothpwex  8636  grothomex  8638  ltexprlem1  8847  ltexprlem4  8850  recexsrlem  8912  lediv2a  9837  lbreu  9891  elfzp12  11057  cau3lem  12086  rlimres  12280  dvdsnegb  12795  dvds2add  12809  dvds2sub  12810  ndvdssub  12855  isfunc  13989  drsdirfi  14323  spweu  14587  gimcnv  14982  gaid  15004  lmhmlem  16033  lmimcnv  16067  abvn0b  16290  prmirredlem  16697  toponcom  16919  neitr  17167  cnprest  17276  nrmsep2  17343  2ndcsep  17444  reghaus  17779  isfil2  17810  alexsubALTlem3  18002  cnextcn  18020  lpbl  18424  iscau4  19104  caussi  19122  cmetcusp  19176  ovolicc2lem3  19283  limcresi  19640  elply2  19983  elqaa  20107  aannenlem1  20113  aannenlem2  20114  bpos1lem  20934  uhgrares  21211  usgrares  21257  usgraexmpl  21287  cusgra3v  21340  cusgrafilem2  21356  redwlk  21455  wlkdvspthlem  21456  cyclispthon  21469  usgrcyclnl1  21476  3v3e3cycl1  21480  eupatrl  21539  isgrpo  21633  gxsub  21713  rngmgmbs4  21854  vcz  21898  sspival  22086  hvsub4  22388  hvaddsub4  22429  5oalem2  23006  5oalem5  23009  5oalem6  23010  3oalem2  23014  homcl  23098  hoadddi  23155  stle0i  23591  spansncv2  23645  mdsymlem1  23755  cdj3lem1  23786  disjin  23872  sxbrsigalem0  24416  dya2icoseg2  24423  ballotlemirc  24569  axcont  25630  colineardim1  25710  idinside  25733  lukshef-ax2  25880  ovoliunnfl  25954  finminlem  26013  ivthALT  26030  indexa  26127  sstotbnd3  26177  heibor1lem  26210  heibor1  26211  eldioph4i  26565  acongtr  26735  aaitgo  27037  dvsconst  27217  stoweidlem17  27435  dmfcoafv  27709  frgraunss  27749  frgranbnb  27774  frgrawopreg  27802  bnj145  28433  bnj168  28436  bnj546  28606  bnj594  28622  bnj1097  28689  bnj1110  28690  bnj1174  28711  bnj1176  28713  ax12olem2wAUX7  28795  exdistrfNEW7  28844  equs45fNEW7  28955  ax12olem2OLD7  29023  dalem53  29840  dalem54  29841  linepsubN  29867  pmapsub  29883  elpaddri  29917  pclfinN  30015  pclcmpatN  30016  cdlemg33c0  30817  dihatexv2  31455
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