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

Theorem anim2i 552
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 19 . 2  |-  ( ch 
->  ch )
2 anim1i.1 . 2  |-  ( ph  ->  ps )
31, 2anim12i 549 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylanl2  632  sylanr2  634  andi  837  sbimi  1642  19.41  1827  ax12olem2  1881  exdistrf  1924  equs45f  1942  eupickb  2221  2eu1  2236  darii  2255  festino  2261  baroco  2262  r19.27av  2694  rspc2ev  2905  reu3  2968  difrab  3455  trssord  4425  ordnbtwn  4499  tfi  4660  find  4697  imainss  5112  fof  5467  f1ocnv  5501  fv3  5557  fvelimab  5594  dff2  5688  dffo5  5693  dff1o6  5807  oprabid  5898  ssoprab2i  5952  ndmovass  6024  ndmovdistr  6025  releldm2  6186  tfrlem5  6412  omlimcl  6592  odi  6593  ixpf  6854  infcntss  7146  hartogs  7275  card2on  7284  epfrs  7429  acni3  7690  dfac2  7773  cflm  7892  axdc2lem  8090  ac6s  8127  ondomon  8201  axregndlem1  8240  axregnd  8242  eltsk2g  8389  grothpw  8464  grothpwex  8465  grothomex  8467  ltexprlem1  8676  ltexprlem4  8679  recexsrlem  8741  lediv2a  9666  lbreu  9720  elfzp12  10877  cau3lem  11854  rlimres  12048  dvdsnegb  12562  dvds2add  12576  dvds2sub  12577  ndvdssub  12622  isfunc  13754  drsdirfi  14088  spweu  14352  gimcnv  14747  gaid  14769  lmhmlem  15802  lmimcnv  15836  abvn0b  16059  prmirredlem  16462  toponcom  16684  cnprest  17033  nrmsep2  17100  2ndcsep  17201  reghaus  17532  isfil2  17567  alexsubALTlem3  17759  lpbl  18065  iscau4  18721  caussi  18739  ovolicc2lem3  18894  limcresi  19251  elply2  19594  elqaa  19718  aannenlem1  19724  aannenlem2  19725  bpos1lem  20537  isgrpo  20879  gxsub  20959  rngmgmbs4  21100  vcz  21142  sspival  21330  hvsub4  21632  hvaddsub4  21673  5oalem2  22250  5oalem5  22253  5oalem6  22254  3oalem2  22258  homcl  22342  hoadddi  22399  stle0i  22835  spansncv2  22889  mdsymlem1  22999  cdj3lem1  23030  xrofsup  23270  xrge0iifhom  23334  disjin  23377  esumc  23445  esumsn  23452  sigaclci  23508  axcont  24676  colineardim1  24756  idinside  24779  lukshef-ax2  24926  ovoliunnfl  25001  sallnei  25632  trnij  25718  cmp2morpcats  26064  abhp  26276  finminlem  26334  ivthALT  26361  indexa  26515  sstotbnd3  26603  heibor1lem  26636  heibor1  26637  eldioph4i  26998  acongtr  27168  aaitgo  27470  dvsconst  27650  stoweidlem17  27869  stoweidlem51  27903  dmfcoafv  28143  usgraexmpl  28267  cusgra3v  28299  trlonprop  28341  redwlk  28364  wlkdvspthlem  28365  cyclispthon  28378  eupatrl  28385  usgrcyclnl1  28386  3v3e3cycl1  28390  bnj145  29071  bnj168  29074  bnj546  29244  bnj594  29260  bnj1097  29327  bnj1110  29328  bnj1174  29349  bnj1176  29351  ax12olem2wAUX7  29433  exdistrfNEW7  29482  equs45fNEW7  29593  ax12olem2OLD7  29660  dalem53  30536  dalem54  30537  linepsubN  30563  pmapsub  30579  elpaddri  30613  pclfinN  30711  pclcmpatN  30712  cdlemg33c0  31513  dihatexv2  32151
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 177  df-an 360
  Copyright terms: Public domain W3C validator