Theorem anim2i 593

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
anim1i.1	|- ( ph -> ps )

Assertion

Ref	Expression
anim2i	|- ( ( ch /\ ph ) -> ( ch /\ ps ) )

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ch -> ch )
2		anim1i.1	. 2 |- ( ph -> ps )
3	1, 2	anim12i 590	1 |- ( ( ch /\ ph ) -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  sylanl2  683  sylanr2  685  andi  911  sbimi  1886  exdistrf  2333  equs45f  2350  moaneu  2533  darii  2565  festino  2571  baroco  2572  r19.27v  3070  rspc2ev  3324  reu3  3396  difrab  3901  copsexg  4956  imainss  5548  trssord  5740  ordnbtwn  5816  ordnbtwnOLD  5817  fof  6115  f1ocnv  6149  fv3  6206  fvelimab  6253  dff2  6371  dffo5  6376  foco2  6379  fnsnb  6432  tpres  6466  f13dfv  6530  dff1o6  6531  oprabid  6677  ssoprab2i  6749  ndmovass  6822  ndmovdistr  6823  elovmpt3rab1  6893  tfi  7053  find  7091  releldm2  7218  bropopvvv  7255  bropfvvvvlem  7256  ressuppssdif  7316  supp0cosupp0  7334  imacosupp  7335  dfrecs3  7469  omlimcl  7658  odi  7659  ixpf  7930  infcntss  8234  funsnfsupp  8299  hartogs  8449  card2on  8459  zfreg  8500  epfrs  8607  acni3  8870  dfac2  8953  cflm  9072  axdc2lem  9270  ac6s  9306  ondomon  9385  axregndlem1  9424  axregnd  9426  eltsk2g  9573  grothpw  9648  grothpwex  9649  grothomex  9651  ltexprlem1  9858  ltexprlem4  9861  recexsrlem  9924  lediv2a  10917  lbreu  10973  elfzp12  12419  dfceil2  12640  focdmex  13139  hashf1rn  13142  hashdifpr  13203  hashge2el2dif  13262  ccatsymb  13366  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12  13491  repswsymball  13526  cshwidxmod  13549  repswcshw  13558  cshimadifsn  13575  cshimadifsn0  13576  wwlktovfo  13701  relexpsucnnl  13772  cau3lem  14094  rlimres  14289  dvdsnegb  14999  dvds2add  15015  dvds2sub  15016  ndvdssub  15133  gcd2n0cl  15231  lcmfun  15358  divgcdcoprmex  15380  cncongr1  15381  powm2modprm  15508  cshwshashlem2  15803  isfunc  16524  drsdirfi  16938  gimcnv  17709  gaid  17732  symg2bas  17818  gsummptnn0fz  18382  lmhmlem  19029  lmimcnv  19067  abvn0b  19302  prmirredlem  19841  psgndiflemB  19946  matbas2  20227  matsubgcell  20240  tposmap  20263  mat1dim0  20279  mat1dimid  20280  mat1dimscm  20281  mat1dimmul  20282  dmatmul  20303  dmatcrng  20308  scmatcrng  20327  scmatf1  20337  1marepvsma1  20389  maducoeval2  20446  smadiadetlem3lem0  20471  slesolinv  20486  cramerimplem1  20489  cramerimplem2  20490  1pmatscmul  20507  cpmatacl  20521  cpmatmcllem  20523  cpmatmcl  20524  mat2pmatf1  20534  mat2pmatghm  20535  mat2pmatmul  20536  mat2pmatlin  20540  mat2pmatscmxcl  20545  m2cpmmhm  20550  m2pmfzgsumcl  20553  m2cpmrngiso  20563  decpmatmul  20577  pmatcollpw2lem  20582  monmatcollpw  20584  pmatcollpwfi  20587  pmatcollpw3fi1lem2  20592  pmatcollpwscmatlem1  20594  pmatcollpwscmatlem2  20595  pmatcollpwscmat  20596  pm2mpghm  20621  pm2mpmhmlem2  20624  pm2mp  20630  chmatcl  20633  chmatval  20634  chmaidscmat  20653  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulcl  20662  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmidgsumm2pm  20674  cpmidpmatlem2  20676  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  cpmadumatpolylem2  20687  cayhamlem2  20689  chcoeffeqlem  20690  cayleyhamilton0  20694  cayleyhamiltonALT  20696  toprntopon  20729  toponcom  20732  neitr  20984  cnprest  21093  nrmsep2  21160  bwth  21213  2ndcsep  21262  isref  21312  reghaus  21628  isfil2  21660  alexsubALTlem3  21853  cnextcn  21871  lpbl  22308  cmodscmulexp  22922  iscau4  23077  caussi  23095  cmetcusp  23150  ovolicc2lem3  23287  limcresi  23649  elply2  23952  elqaa  24077  aannenlem1  24083  aannenlem2  24084  relogbreexp  24513  cxplogb  24524  bpos1lem  25007  lgsqrmodndvds  25078  axcont  25856  usgrexmplef  26151  subupgr  26179  cplgr3v  26331  cusgrfilem2  26352  usgredgsscusgredg  26355  rusgrprop0  26463  uspgr2wlkeqi  26544  spthonpthon  26647  usgr2wlkspthlem1  26653  usgr2wlkspthlem2  26654  usgr2trlncl  26656  clwlkcompim  26676  clwlkl1loop  26678  wlkwwlkinj  26782  wwlksnred  26787  wwlksnextbi  26789  wwlksnfi  26801  clwwlknclwwlkdifs  26873  clwlksf1clwwlklem0  26964  clwwlksnun  26974  1pthon2v  27013  frcond1  27130  frcond4  27134  frgrnbnb  27157  extwwlkfab  27223  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwwlk2  27240  frgrregord013  27253  isgrpo  27351  vcz  27430  hvsub4  27894  hvaddsub4  27935  5oalem2  28514  5oalem5  28517  5oalem6  28518  3oalem2  28522  homcl  28605  hoadddi  28662  stle0i  29098  spansncv2  29152  mdsymlem1  29262  cdj3lem1  29293  disjin  29399  disjin2  29400  f1ocnt  29559  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  pmtrprfv2  29848  crefdf  29915  sxbrsigalem0  30333  dya2icoseg2  30340  eulerpartlemgvv  30438  ballotlemirc  30593  bnj145OLD  30795  bnj168  30798  bnj546  30966  bnj594  30982  bnj1097  31049  bnj1110  31050  bnj1174  31071  bnj1176  31073  fv1stcnv  31680  noetalem5  31867  colineardim1  32168  idinside  32191  finminlem  32312  ivthALT  32330  lukshef-ax2  32414  bj-19.41al  32637  bj-equs45fv  32752  bj-rest10b  33042  bj-ccinftydisj  33100  mptsnunlem  33185  topdifinffinlem  33195  relowlssretop  33211  elxp8  33219  matunitlindflem1  33405  poimirlem22  33431  poimirlem25  33434  poimirlem27  33436  poimirlem31  33440  ovoliunnfl  33451  itg2addnclem  33461  indexa  33528  sstotbnd3  33575  heibor1lem  33608  heibor1  33609  rngmgmbs4  33730  exmid2  33901  dalem53  35011  dalem54  35012  linepsubN  35038  pmapsub  35054  elpaddri  35088  pclfinN  35186  pclcmpatN  35187  cdlemg33c0  35990  dihatexv2  36628  eldioph4i  37376  acongtr  37545  pwfi2f1o  37666  aaitgo  37732  frege54cor0a  38157  clsf2  38424  dvsconst  38529  xlimxrre  40057  icccncfext  40100  stoweidlem17  40234  elaa2  40451  dmfcoafv  41255  elfzelfzlble  41331  pfxn0  41394  swrdpfx  41414  pfxpfx  41415  pfxccatin12lem2  41424  pfxccatin12  41425  repswpfx  41436  pfxco  41438  fmtnoprmfac1  41477  fmtnoprmfac2  41479  flsqrt  41508  lighneallem3  41524  proththd  41531  evenprm2  41623  gbogbow  41644  uspgrsprfo  41756  c0mgm  41909  c0rhm  41912  rhmisrnghm  41920  lidlmmgm  41925  2zrngnmrid  41950  rhmsubcrngclem1  42027  srhmsubclem1  42073  rhmsubcALTVlem3  42106  linccl  42203  lincvalpr  42207  lincdifsn  42213  lincext1  42243  lindslinindsimp1  42246  ldepspr  42262  lincresunit3lem1  42268  logblt1b  42358  dignnld  42397  dig1  42402  dignn0flhalflem1  42409  amgmwlem  42548