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  1633  19.41  1815  ax12olem2  1869  exdistrf  1911  equs45f  1929  eupickb  2208  2eu1  2223  darii  2242  festino  2248  baroco  2249  r19.27av  2681  rspc2ev  2892  reu3  2955  difrab  3442  trssord  4409  ordnbtwn  4483  tfi  4644  find  4681  imainss  5096  fof  5451  f1ocnv  5485  fv3  5541  fvelimab  5578  dff2  5672  dffo5  5677  dff1o6  5791  oprabid  5882  ssoprab2i  5936  ndmovass  6008  ndmovdistr  6009  releldm2  6170  tfrlem5  6396  omlimcl  6576  odi  6577  ixpf  6838  infcntss  7130  hartogs  7259  card2on  7268  epfrs  7413  acni3  7674  dfac2  7757  cflm  7876  axdc2lem  8074  ac6s  8111  ondomon  8185  axregndlem1  8224  axregnd  8226  eltsk2g  8373  grothpw  8448  grothpwex  8449  grothomex  8451  ltexprlem1  8660  ltexprlem4  8663  recexsrlem  8725  lediv2a  9650  lbreu  9704  elfzp12  10861  cau3lem  11838  rlimres  12032  dvdsnegb  12546  dvds2add  12560  dvds2sub  12561  ndvdssub  12606  isfunc  13738  drsdirfi  14072  spweu  14336  gimcnv  14731  gaid  14753  lmhmlem  15786  lmimcnv  15820  abvn0b  16043  prmirredlem  16446  toponcom  16668  cnprest  17017  nrmsep2  17084  2ndcsep  17185  reghaus  17516  isfil2  17551  alexsubALTlem3  17743  lpbl  18049  iscau4  18705  caussi  18723  ovolicc2lem3  18878  limcresi  19235  elply2  19578  elqaa  19702  aannenlem1  19708  aannenlem2  19709  bpos1lem  20521  isgrpo  20863  gxsub  20943  rngmgmbs4  21084  vcz  21126  sspival  21314  hvsub4  21616  hvaddsub4  21657  5oalem2  22234  5oalem5  22237  5oalem6  22238  3oalem2  22242  homcl  22326  hoadddi  22383  stle0i  22819  spansncv2  22873  mdsymlem1  22983  cdj3lem1  23014  xrofsup  23255  xrge0iifhom  23319  disjin  23362  esumc  23430  esumsn  23437  sigaclci  23493  axcont  24604  colineardim1  24684  idinside  24707  lukshef-ax2  24854  sallnei  25529  trnij  25615  cmp2morpcats  25961  abhp  26173  finminlem  26231  ivthALT  26258  indexa  26412  sstotbnd3  26500  heibor1lem  26533  heibor1  26534  eldioph4i  26895  acongtr  27065  aaitgo  27367  dvsconst  27547  stoweidlem17  27766  stoweidlem51  27800  dmfcoafv  28036  usgraexmpl  28133  bnj145  28755  bnj168  28758  bnj546  28928  bnj594  28944  bnj1097  29011  bnj1110  29012  bnj1174  29033  bnj1176  29035  dalem53  29914  dalem54  29915  linepsubN  29941  pmapsub  29957  elpaddri  29991  pclfinN  30089  pclcmpatN  30090  cdlemg33c0  30891  dihatexv2  31529
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