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  2419  ordelinel  4976  fores  5802  ssimaex  5930  dffv2  5938  exfo  6037  oprabv  6327  ndmovass  6445  fun11uni  6735  fabexg  6737  f1oabexg  6740  fun11iun  6741  soxp  6893  tz7.48lem  7103  tz7.49c  7108  omass  7226  oewordri  7238  omabs  7293  sbthlem9  7632  fineqvlem  7731  pssnn  7735  domunfican  7789  fiint  7793  fsuppsssupp  7841  inf1  8035  infeq5  8050  cantnfle  8086  rankuni  8277  acndom  8428  acnnum  8429  cdainflem  8567  cfcof  8650  ac6num  8855  ac6s2  8862  brdom5  8903  brdom4  8904  genpnnp  9379  lediv2a  10435  supmul1  10504  nn2ge  10557  btwnz  10959  eluz2b2  11150  uz2mulcl  11155  eqreznegel  11163  xrsupexmnf  11492  xrinfmexpnf  11493  xrsupsslem  11494  xrinfmsslem  11495  supxrun  11503  ioo0  11550  elioo4g  11581  fz0fzelfz0  11774  fz0fzdiffz0  11777  2ffzeq  11787  elfzodifsumelfzo  11846  elfzom1elp1fzo  11847  zpnn0elfzo  11852  fzonfzoufzol  11877  quoremnn0  11947  zmodidfzoimp  11990  modabs  11993  modifeq2int  12013  modaddmulmod  12017  expcl2lem  12142  ccatw2s1p1  12599  ccatw2s1p2  12600  swrdspsleq  12632  swrd0swrd  12645  swrdccatin2  12671  swrdccatin12lem3  12674  swrdccat3  12676  swrdccat3blem  12679  swrdccatid  12681  repswccat  12716  2cshw  12740  cshweqdifid  12747  lswco  12763  repsco  12764  s4f1o  12825  ccat2s1fvwALT  12852  mulre  12913  rediv  12923  imdiv  12930  resqrex  13043  caurcvg2  13459  modfsummods  13566  tanval  13720  negdvdsb  13857  muldvds1  13865  muldvds2  13866  dvdscmulr  13869  dvdsmulcr  13870  divalglem8  13913  maxprmfct  14109  modprm0  14185  modprmn0modprm0  14187  pcpremul  14222  pcmul  14230  cshwsidrepsw  14432  gsmsymgreqlem2  16251  symgfixfo  16260  fsfnn0gsumfsffz  16802  irredn0  17136  rim0to0  17174  lsppratlem1  17576  ixpsnbasval  17638  cply1coe0bi  18113  dvdsrzring  18274  dvdsrz  18275  matinvgcell  18704  mat1dimcrng  18746  dmatscmcl  18772  scmatmats  18780  scmatscm  18782  scmatmulcl  18787  scmatghm  18802  scmatmhm  18803  ma1repvcl  18839  mdet1  18870  mdet0  18875  slesolinv  18949  slesolinvbi  18950  cramerimplem1  18952  cramerimp  18955  cramerlem1  18956  cramer  18960  cpmatacl  18984  cpmatmcl  18987  mat2pmatghm  18998  mat2pmatmul  18999  m2pmfzgsumcl  19016  decpmatmul  19040  decpmatmulsumfsupp  19041  pmatcollpwfi  19050  pmatcollpwscmat  19059  pm2mpf1  19067  pm2mpghm  19084  pm2mpmhmlem1  19086  monmat2matmon  19092  chpdmatlem2  19107  chpdmat  19109  chfacfisf  19122  cpmadugsumlemB  19142  cpmadugsumlemC  19143  cpmadugsumlemF  19144  clscld  19314  neiptopnei  19399  2ndcdisj2  19724  tx1stc  19886  opnfbas  20078  fbasfip  20104  alexsublem  20279  alexsubALTlem4  20285  cnextcn  20302  bcthlem5  21502  vitalilem4  21755  vitalilem5  21756  itg2mulc  21889  itg2monolem1  21892  itg2monolem2  21893  itg2monolem3  21894  itg2mono  21895  itg2i1fseqle  21896  itg2i1fseq3  21899  itg2addlem  21900  itg2gt0  21902  itg2cnlem2  21904  dvcobr  22084  dvcnvlem  22112  dvferm1  22121  dvne0  22147  mdegmullem  22213  plyeq0lem  22342  plyexmo  22443  aalioulem5  22466  aalioulem6  22467  aaliou  22468  cxple2a  22808  cxpaddlelem  22853  cxpaddle  22854  bcmono  23280  lgsquadlem2  23358  xmstrkgc  23865  colinearalg  23889  axcontlem3  23945  usgraexmpl  24077  nb3grapr  24129  nb3grapr2  24130  nb3gra2nb  24131  cusgrarn  24135  cusgrasizeindslem3  24151  spthonepeq  24265  fargshiftfva  24315  wlkiswwlksur  24395  clwwlknimp  24452  clwlkisclwwlklem2a  24461  clwlkisclwwlklem0  24464  wwlksubclwwlk  24480  clwwisshclww  24483  clwwnisshclwwn  24485  eleclclwwlknlem2  24494  usg2spthonot1  24566  vdusgraval  24583  cusgraisrusgra  24614  rusgranumwlk  24633  eupatrl  24644  1to3vfriswmgra  24683  frgranbnb  24696  vdfrgra0  24698  vdgfrgra0  24699  vdgn0frgrav2  24701  vdgn1frgrav2  24703  frgrawopreg  24726  frg2wot1  24734  usg2spot2nb  24742  frgraregorufrg  24749  numclwwlkovfel2  24760  numclwlk1lem2foa  24768  numclwlk1lem2fv  24770  numclwwlk1  24775  numclwlk2lem2fv  24781  numclwwlk4  24787  numclwwlk5  24789  numclwwlk6  24790  frgrareg  24794  frgraregord013  24795  ex-natded9.20-2  24816  grpoidinvlem3  24884  grpoidinv  24886  ablomul  25033  isdivrngo  25109  sspival  25327  nmobndseqi  25370  nmobndseqiOLD  25371  hvaddsub4  25671  hhcmpl  25793  ocsh  25877  5oalem2  26249  5oalem5  26252  3oalem2  26257  pjjsi  26294  hoadddir  26399  leopmul  26729  stge1i  26833  hatomistici  26957  mdsymlem2  26999  mdsymlem5  27002  addltmulALT  27041  isoun  27192  qqhre  27634  sxbrsigalem0  27882  dya2iocnei  27893  sxbrsigalem5  27899  sibfinima  27921  eulerpartlemgs2  27959  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemsup  28083  cvmsi  28350  elno2  28991  nobndlem6  29034  trisegint  29255  funtransport  29258  btwnconn1lem4  29317  btwnconn2  29329  segcon2  29332  outsideofeu  29358  lukshef-ax2  29457  limsucncmpi  29487  heicant  29626  ismblfin  29632  itg2addnc  29646  itg2gt0cn  29647  bddiblnc  29662  ftc1anclem6  29672  ftc1anclem8  29674  ftc1anc  29675  areacirc  29689  isfne  29740  comppfsc  29779  opelopab3  29810  isdrngo2  29964  fldcrng  30004  flddmn  30058  orel  30107  cmpfiiin  30233  pellexlem4  30372  pellqrex  30419  acongtr  30520  acongrep  30522  jm2.23  30542  pm10.55  30852  refsum2cnlem1  30990  fmuldfeq  31133  climsuse  31150  limclner  31193  icccncfext  31226  stoweidlem26  31326  stoweidlem52  31352  stoweidlem57  31357  fourierdlem20  31427  fourierdlem41  31448  fourierdlem52  31459  fourierdlem74  31481  fourierdlem75  31482  fourierdlem102  31509  fourierdlem114  31521  afvelrn  31720  elpwdifsn  31763  lesubnn0  31795  elfz2z  31800  2ffzoeq  31810  ccatw2s1cl  31813  edgssv2ALT  31870  edgssv2  31871  usgfislem2  31914  usgfisALTlem2  31918  assintop  31956  lmodvsmdi  32048  lincsum  32103  lincsumcl  32105  el0ldep  32140  ldepspr  32147  lindssnlvec  32160  bnj529  32877  bnj945  32911  bnj1098  32921  bnj1533  32989  bnj605  33044  bnj594  33049  bnj607  33053  bnj966  33081  bnj967  33082  bnj996  33092  bnj999  33094  bnj1006  33096  bnj1118  33119  bnj1172  33136  bnj1279  33153  bnj1296  33156  bnj1498  33196  cmtbr4N  34052  linepsubN  34548  pmapsub  34564  paddasslem14  34629  pclcmpatN  34697  trlval2  34959  cdleme20  35120  cdleme21j  35132  dvalveclem  35822  dia2dimlem7  35867  dvhlveclem  35905  docaclN  35921  dihjat1  36226  mapdhcl  36524  mapdh6dN  36536  mapdh8  36586  hdmap1l6d  36611  hdmap10  36640  hdmaprnlem17N  36663  hdmaplkr  36713  hdmapip0  36715  hgmapvv  36726