Theorem anim1i 572

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

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  sylanl1  656  sylanr1  658  disamis  2405  fores  5802  ssimaex  5930  dffv2  5938  exfo  6040  oprabv  6339  ndmovass  6457  fun11uni  6747  fabexg  6749  f1oabexg  6752  fun11iun  6753  soxp  6909  tz7.48lem  7158  tz7.49c  7163  omass  7281  oewordri  7293  omabs  7348  sbthlem9  7690  fineqvlem  7786  pssnn  7790  domunfican  7844  fiint  7848  fsuppsssupp  7899  sup0  7980  inf1  8127  infeq5  8142  cantnfle  8176  rankuni  8334  acndom  8482  acnnum  8483  cdainflem  8621  cfcof  8704  ac6num  8909  ac6s2  8916  brdom5  8957  brdom4  8958  genpnnp  9430  lediv2a  10500  supmul1  10576  infregelb  10594  nn2ge  10634  btwnz  11037  eluz2b2  11231  uz2mulcl  11236  eqreznegel  11249  xrsupexmnf  11590  xrinfmexpnf  11591  xrsupsslem  11592  xrinfmsslem  11593  supxrun  11601  ioo0  11661  elioo4g  11695  fz0fzelfz0  11896  fz0fzdiffz0  11899  2ffzeq  11910  elfzodifsumelfzo  11980  elfzom1elp1fzo  11981  zpnn0elfzo  11986  fzonfzoufzol  12012  quoremnn0  12083  zmodidfzoimp  12127  modabs  12130  modifeq2int  12152  modaddmulmod  12156  expcl2lem  12284  ccatcl  12720  ccatval3  12724  swrdfv2  12802  swrdsbslen  12804  swrdspsleq  12805  swrd0swrd  12817  swrdccatin2  12843  swrdccatin12lem3  12846  swrdccat3  12848  swrdccat3blem  12851  swrdccatid  12853  repswccat  12888  2cshw  12912  cshweqdifid  12919  lswco  12935  repsco  12936  s4f1o  13003  ccat2s1fvwALT  13030  trclun  13078  mulre  13184  rediv  13194  imdiv  13201  resqrex  13314  caurcvg2  13744  modfsummods  13853  tanval  14182  negdvdsb  14319  muldvds1  14327  muldvds2  14328  dvdscmulr  14331  dvdsmulcr  14332  divalglem8  14380  lcmfunsnlem2lem2  14612  lcmfun  14618  maxprmfct  14652  coprmgcdb  14654  ncoprmgcdne1b  14655  ncoprmlnprm  14677  vfermltl  14752  vfermltlALT  14753  modprm0  14756  modprmn0modprm0  14758  pcpremul  14793  pcmul  14801  prmdvdsprmo  15000  prmdvdsprmorOLD  15015  prmgaplem4  15024  prmgaplem7  15027  cshwsidrepsw  15064  gsmsymgreqlem2  17072  symgfixfo  17080  fsfnn0gsumfsffz  17612  irredn0  17931  rim0to0  17970  lsppratlem1  18370  ixpsnbasval  18432  cply1coe0bi  18894  dvdsrzring  19052  matinvgcell  19460  mat1dimcrng  19502  dmatscmcl  19528  scmatmats  19536  scmatscm  19538  scmatmulcl  19543  scmatghm  19558  scmatmhm  19559  ma1repvcl  19595  mdet1  19626  mdet0  19631  slesolinv  19705  slesolinvbi  19706  cramerimplem1  19708  cramerimp  19711  cramerlem1  19712  cramer  19716  cpmatacl  19740  cpmatmcl  19743  mat2pmatghm  19754  mat2pmatmul  19755  m2pmfzgsumcl  19772  decpmatmul  19796  decpmatmulsumfsupp  19797  pmatcollpwfi  19806  pmatcollpwscmat  19815  pm2mpf1  19823  pm2mpghm  19840  pm2mpmhmlem1  19842  monmat2matmon  19848  chpdmatlem2  19863  chpdmat  19865  chfacfisf  19878  cpmadugsumlemB  19898  cpmadugsumlemC  19899  cpmadugsumlemF  19900  clscld  20062  neiptopnei  20148  2ndcdisj2  20472  comppfsc  20547  tx1stc  20665  opnfbas  20857  fbasfip  20883  alexsublem  21059  alexsubALTlem4  21065  cnextcn  21082  bcthlem5  22296  vitalilem4  22569  vitalilem5  22570  itg2mulc  22705  dvcobr  22900  dvcnvlem  22928  dvferm1  22937  dvne0  22963  mdegmullem  23027  plyeq0lem  23164  plyexmo  23266  aalioulem5  23292  aalioulem6  23293  aaliou  23294  cxple2a  23644  cxpaddlelem  23691  cxpaddle  23692  relogbcxpb  23724  bcmono  24205  lgsquadlem2  24283  colinearalg  24940  axcontlem3  24996  usgraexmplef  25128  nb3grapr  25181  nb3grapr2  25182  nb3gra2nb  25183  cusgrarn  25187  cusgrasizeindslem3  25203  spthonepeq  25317  fargshiftfva  25367  wlkiswwlksur  25447  clwwlknimp  25504  clwlkisclwwlklem2a  25513  clwlkisclwwlklem0  25516  wwlksubclwwlk  25532  clwwisshclww  25535  clwwnisshclwwn  25537  eleclclwwlknlem2  25546  usg2spthonot1  25618  vdusgraval  25635  cusgraisrusgra  25666  rusgranumwlk  25685  eupatrl  25696  1to3vfriswmgra  25735  frgranbnb  25748  vdfrgra0  25750  vdgn0frgrav2  25752  vdgn1frgrav2  25754  frgrawopreg  25777  frg2wot1  25785  usg2spot2nb  25793  frgraregorufrg  25800  numclwwlkovfel2  25811  numclwlk1lem2foa  25819  numclwlk1lem2fv  25821  numclwwlk1  25826  numclwlk2lem2fv  25832  numclwwlk4  25838  numclwwlk5  25840  numclwwlk6  25841  frgrareg  25845  frgraregord013  25846  ex-natded9.20-2  25868  grpoidinvlem3  25934  grpoidinv  25936  isdivrngo  26159  sspival  26377  nmobndseqi  26420  nmobndseqiALT  26421  hvaddsub4  26731  hhcmpl  26853  ocsh  26936  5oalem2  27308  5oalem5  27311  3oalem2  27316  pjjsi  27353  hoadddir  27457  leopmul  27787  stge1i  27891  hatomistici  28015  mdsymlem2  28057  mdsymlem5  28060  addltmulALT  28099  isoun  28282  crefdf  28675  qqhre  28824  esumiun  28915  sxbrsigalem0  29093  dya2iocnei  29104  sxbrsigalem5  29110  sibfinima  29172  eulerpartlemgs2  29213  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemsup  29337  ballotlemsupOLD  29375  bnj529  29551  bnj945  29585  bnj1098  29595  bnj1533  29663  bnj605  29718  bnj594  29723  bnj607  29727  bnj966  29755  bnj967  29756  bnj996  29766  bnj999  29768  bnj1006  29770  bnj1118  29793  bnj1172  29810  bnj1279  29827  bnj1296  29830  bnj1498  29870  cvmsi  29988  fv2ndcnv  30423  elno2  30541  nobndlem6  30586  trisegint  30795  funtransport  30798  btwnconn1lem4  30857  btwnconn2  30869  segcon2  30872  outsideofeu  30898  isfne  30995  lukshef-ax2  31075  limsucncmpi  31105  bj-elid3  31642  bj-eldiag2  31647  poimirlem26  31966  poimirlem27  31967  poimirlem29  31969  poimirlem30  31970  poimirlem32  31972  heicant  31975  ismblfin  31981  itg2gt0cn  31997  bddiblnc  32012  areacirc  32037  opelopab3  32043  isdrngo2  32197  fldcrng  32237  flddmn  32291  cmtbr4N  32821  linepsubN  33317  pmapsub  33333  paddasslem14  33398  pclcmpatN  33466  trlval2  33729  cdleme20  33891  cdleme21j  33903  dvalveclem  34593  dia2dimlem7  34638  dvhlveclem  34676  docaclN  34692  dihjat1  34997  mapdhcl  35295  mapdh6dN  35307  mapdh8  35357  hdmap1l6d  35382  hdmap10  35411  hdmaprnlem17N  35434  hdmaplkr  35484  hdmapip0  35486  hgmapvv  35497  cmpfiiin  35539  pellexlem4  35676  pellqrex  35726  acongtr  35828  acongrep  35830  jm2.23  35851  rp-fakeanorass  36157  rp-isfinite6  36163  inintabss  36184  pm10.55  36718  refsum2cnlem1  37358  fmuldfeq  37661  climsuse  37687  limclner  37732  icccncfext  37765  stoweidlem26  37886  stoweidlem52  37913  stoweidlem57  37918  fourierdlem20  37989  fourierdlem41  38011  fourierdlem52  38022  fourierdlem64  38034  fourierdlem102  38072  fourierdlem114  38084  afvelrn  38670  opoeALTV  38812  evensumeven  38834  sgoldbalt  38882  evengpop3  38893  evengpoap3  38894  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  tgoldbach  38911  proththd  38914  ccatpfx  38950  pfxccat3  38967  pfxccatpfx2  38969  pfxccat3a  38970  reuccatpfxs1  38975  elpwdifsn  38990  fpropnf1  39036  lesubnn0  39050  elfz2z  39055  2ffzoeq  39064  edgupgr  39225  usgruspgrb  39268  edgassv2  39281  uspgredg2v  39301  subupgr  39359  subusgr  39361  usgrfilem  39393  dfnbgr2  39407  nbupgrres  39438  nb3gr2nb  39458  nbupgruvtxres  39480  cplgr3v  39502  cusgrres  39509  cusgrsizeindslem  39512  cusgrsizeinds  39513  vtxduhgrun  39538  cusgrrusgr  39597  edgssv2ALT  39766  edgssv2  39767  usgfislem2  39810  usgfisALTlem2  39814  assintop  39898  isringrng  39934  rnglz  39937  c0snmgmhm  39967  zrrnghm  39970  uzlidlring  39982  2zrngnmrid  40003  cznrng  40010  rnghmsubcsetclem2  40031  rhmsubcsetclem2  40077  rhmsubcrngclem2  40083  lmodvsmdi  40220  lincsum  40275  lincsumcl  40277  el0ldep  40312  ldepspr  40319  lindssnlvec  40332  modn0mul  40376  m1modmmod  40377  elbigolo1  40421  nn0digval  40464  aacllem  40593