Theorem anim1i 568

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
anim1i	|- ( ( ph /\ ch ) -> ( ps /\ ch ) )

Proof of Theorem anim1i

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sylanl1  650  sylanr1  652  disamis  2393  fores  5791  ssimaex  5920  dffv2  5928  exfo  6031  oprabv  6327  ndmovass  6445  fun11uni  6736  fabexg  6738  f1oabexg  6741  fun11iun  6742  soxp  6895  tz7.48lem  7105  tz7.49c  7110  omass  7228  oewordri  7240  omabs  7295  sbthlem9  7634  fineqvlem  7733  pssnn  7737  domunfican  7792  fiint  7796  fsuppsssupp  7844  inf1  8039  infeq5  8054  cantnfle  8090  rankuni  8281  acndom  8432  acnnum  8433  cdainflem  8571  cfcof  8654  ac6num  8859  ac6s2  8866  brdom5  8907  brdom4  8908  genpnnp  9383  lediv2a  10442  supmul1  10511  nn2ge  10564  btwnz  10968  eluz2b2  11160  uz2mulcl  11165  eqreznegel  11173  xrsupexmnf  11502  xrinfmexpnf  11503  xrsupsslem  11504  xrinfmsslem  11505  supxrun  11513  ioo0  11560  elioo4g  11591  fz0fzelfz0  11785  fz0fzdiffz0  11788  2ffzeq  11799  elfzodifsumelfzo  11858  elfzom1elp1fzo  11859  zpnn0elfzo  11864  fzonfzoufzol  11889  quoremnn0  11959  zmodidfzoimp  12002  modabs  12005  modifeq2int  12025  modaddmulmod  12029  expcl2lem  12154  ccatw2s1p1  12616  ccatw2s1p2  12617  swrdspsleq  12649  swrd0swrd  12662  swrdccatin2  12688  swrdccatin12lem3  12691  swrdccat3  12693  swrdccat3blem  12696  swrdccatid  12698  repswccat  12733  2cshw  12757  cshweqdifid  12764  lswco  12780  repsco  12781  s4f1o  12842  ccat2s1fvwALT  12869  mulre  12930  rediv  12940  imdiv  12947  resqrex  13060  caurcvg2  13476  modfsummods  13583  tanval  13737  negdvdsb  13874  muldvds1  13882  muldvds2  13883  dvdscmulr  13886  dvdsmulcr  13887  divalglem8  13932  maxprmfct  14128  modprm0  14204  modprmn0modprm0  14206  pcpremul  14241  pcmul  14249  cshwsidrepsw  14452  gsmsymgreqlem2  16327  symgfixfo  16335  fsfnn0gsumfsffz  16882  irredn0  17223  rim0to0  17262  lsppratlem1  17664  ixpsnbasval  17726  cply1coe0bi  18213  dvdsrzring  18377  dvdsrz  18378  matinvgcell  18807  mat1dimcrng  18849  dmatscmcl  18875  scmatmats  18883  scmatscm  18885  scmatmulcl  18890  scmatghm  18905  scmatmhm  18906  ma1repvcl  18942  mdet1  18973  mdet0  18978  slesolinv  19052  slesolinvbi  19053  cramerimplem1  19055  cramerimp  19058  cramerlem1  19059  cramer  19063  cpmatacl  19087  cpmatmcl  19090  mat2pmatghm  19101  mat2pmatmul  19102  m2pmfzgsumcl  19119  decpmatmul  19143  decpmatmulsumfsupp  19144  pmatcollpwfi  19153  pmatcollpwscmat  19162  pm2mpf1  19170  pm2mpghm  19187  pm2mpmhmlem1  19189  monmat2matmon  19195  chpdmatlem2  19210  chpdmat  19212  chfacfisf  19225  cpmadugsumlemB  19245  cpmadugsumlemC  19246  cpmadugsumlemF  19247  clscld  19418  neiptopnei  19503  2ndcdisj2  19828  comppfsc  19903  tx1stc  20021  opnfbas  20213  fbasfip  20239  alexsublem  20414  alexsubALTlem4  20420  cnextcn  20437  bcthlem5  21637  vitalilem4  21890  vitalilem5  21891  itg2mulc  22024  dvcobr  22219  dvcnvlem  22247  dvferm1  22256  dvne0  22282  mdegmullem  22348  plyeq0lem  22477  plyexmo  22578  aalioulem5  22601  aalioulem6  22602  aaliou  22603  cxple2a  22949  cxpaddlelem  22994  cxpaddle  22995  bcmono  23421  lgsquadlem2  23499  colinearalg  24082  axcontlem3  24138  usgraexmpl  24270  nb3grapr  24322  nb3grapr2  24323  nb3gra2nb  24324  cusgrarn  24328  cusgrasizeindslem3  24344  spthonepeq  24458  fargshiftfva  24508  wlkiswwlksur  24588  clwwlknimp  24645  clwlkisclwwlklem2a  24654  clwlkisclwwlklem0  24657  wwlksubclwwlk  24673  clwwisshclww  24676  clwwnisshclwwn  24678  eleclclwwlknlem2  24687  usg2spthonot1  24759  vdusgraval  24776  cusgraisrusgra  24807  rusgranumwlk  24826  eupatrl  24837  1to3vfriswmgra  24876  frgranbnb  24889  vdfrgra0  24891  vdgn0frgrav2  24893  vdgn1frgrav2  24895  frgrawopreg  24918  frg2wot1  24926  usg2spot2nb  24934  frgraregorufrg  24941  numclwwlkovfel2  24952  numclwlk1lem2foa  24960  numclwlk1lem2fv  24962  numclwwlk1  24967  numclwlk2lem2fv  24973  numclwwlk4  24979  numclwwlk5  24981  numclwwlk6  24982  frgrareg  24986  frgraregord013  24987  ex-natded9.20-2  25008  grpoidinvlem3  25077  grpoidinv  25079  isdivrngo  25302  sspival  25520  nmobndseqi  25563  nmobndseqiOLD  25564  hvaddsub4  25864  hhcmpl  25986  ocsh  26070  5oalem2  26442  5oalem5  26445  3oalem2  26450  pjjsi  26487  hoadddir  26592  leopmul  26922  stge1i  27026  hatomistici  27150  mdsymlem2  27192  mdsymlem5  27195  addltmulALT  27234  isoun  27389  crefdf  27721  qqhre  27868  sxbrsigalem0  28112  dya2iocnei  28123  sxbrsigalem5  28129  sibfinima  28151  eulerpartlemgs2  28189  ballotlemfc0  28301  ballotlemfcc  28302  ballotlemsup  28313  cvmsi  28580  elno2  29386  nobndlem6  29429  trisegint  29650  funtransport  29653  btwnconn1lem4  29712  btwnconn2  29724  segcon2  29727  outsideofeu  29753  lukshef-ax2  29852  limsucncmpi  29882  heicant  30021  ismblfin  30027  itg2gt0cn  30042  bddiblnc  30057  areacirc  30084  isfne  30129  opelopab3  30179  isdrngo2  30333  fldcrng  30373  flddmn  30427  cmpfiiin  30601  pellexlem4  30740  pellqrex  30787  acongtr  30888  acongrep  30890  jm2.23  30910  pm10.55  31225  refsum2cnlem1  31363  fmuldfeq  31505  climsuse  31522  limclner  31565  icccncfext  31597  stoweidlem26  31697  stoweidlem52  31723  stoweidlem57  31728  fourierdlem20  31798  fourierdlem41  31819  fourierdlem52  31830  fourierdlem64  31842  fourierdlem102  31880  fourierdlem114  31892  afvelrn  32091  elpwdifsn  32134  lesubnn0  32164  elfz2z  32169  2ffzoeq  32179  edgssv2ALT  32239  edgssv2  32240  usgfislem2  32283  usgfisALTlem2  32287  assintop  32370  isringrng  32405  uzlidlring  32442  2zrngnmrid  32463  cznrng  32470  rnghmsubcsetclem2  32521  rhmsubcsetclem2  32562  rhmsubcrngclem2  32568  lmodvsmdi  32705  lincsum  32760  lincsumcl  32762  el0ldep  32797  ldepspr  32804  lindssnlvec  32817  bnj529  33526  bnj945  33560  bnj1098  33570  bnj1533  33638  bnj605  33693  bnj594  33698  bnj607  33702  bnj966  33730  bnj967  33731  bnj996  33741  bnj999  33743  bnj1006  33745  bnj1118  33768  bnj1172  33785  bnj1279  33802  bnj1296  33805  bnj1498  33845  cmtbr4N  34703  linepsubN  35199  pmapsub  35215  paddasslem14  35280  pclcmpatN  35348  trlval2  35611  cdleme20  35773  cdleme21j  35785  dvalveclem  36475  dia2dimlem7  36520  dvhlveclem  36558  docaclN  36574  dihjat1  36879  mapdhcl  37177  mapdh6dN  37189  mapdh8  37239  hdmap1l6d  37264  hdmap10  37293  hdmaprnlem17N  37316  hdmaplkr  37366  hdmapip0  37368  hgmapvv  37379  rp-fakeanorass  37423  rp-isfinite6  37430