Theorem anim1i 570

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 23	. 2 |- ( ch -> ch )
3	1, 2	anim12i 568	1 |- ( ( ph /\ ch ) -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  sylanl1  654  sylanr1  656  disamis  2372  fores  5810  ssimaex  5937  dffv2  5945  exfo  6046  oprabv  6344  ndmovass  6462  fun11uni  6752  fabexg  6754  f1oabexg  6757  fun11iun  6758  soxp  6911  tz7.48lem  7157  tz7.49c  7162  omass  7280  oewordri  7292  omabs  7347  sbthlem9  7687  fineqvlem  7783  pssnn  7787  domunfican  7841  fiint  7845  fsuppsssupp  7896  sup0  7977  inf1  8118  infeq5  8133  cantnfle  8166  rankuni  8324  acndom  8471  acnnum  8472  cdainflem  8610  cfcof  8693  ac6num  8898  ac6s2  8905  brdom5  8946  brdom4  8947  genpnnp  9419  lediv2a  10489  supmul1  10565  infregelb  10583  nn2ge  10623  btwnz  11026  eluz2b2  11220  uz2mulcl  11225  eqreznegel  11238  xrsupexmnf  11579  xrinfmexpnf  11580  xrsupsslem  11581  xrinfmsslem  11582  supxrun  11590  ioo0  11650  elioo4g  11684  fz0fzelfz0  11883  fz0fzdiffz0  11886  2ffzeq  11897  elfzodifsumelfzo  11966  elfzom1elp1fzo  11967  zpnn0elfzo  11972  fzonfzoufzol  11998  quoremnn0  12069  zmodidfzoimp  12113  modabs  12116  modifeq2int  12138  modaddmulmod  12142  expcl2lem  12270  ccatcl  12696  ccatval3  12700  swrdfv2  12776  swrdsbslen  12778  swrdspsleq  12779  swrd0swrd  12791  swrdccatin2  12817  swrdccatin12lem3  12820  swrdccat3  12822  swrdccat3blem  12825  swrdccatid  12827  repswccat  12862  2cshw  12886  cshweqdifid  12893  lswco  12909  repsco  12910  s4f1o  12971  ccat2s1fvwALT  12998  trclun  13046  mulre  13152  rediv  13162  imdiv  13169  resqrex  13282  caurcvg2  13711  modfsummods  13820  tanval  14149  negdvdsb  14286  muldvds1  14294  muldvds2  14295  dvdscmulr  14298  dvdsmulcr  14299  divalglem8  14345  lcmfunsnlem2lem2  14572  lcmfun  14578  maxprmfct  14612  coprmgcdb  14614  ncoprmgcdne1b  14615  ncoprmlnprm  14637  vfermltl  14704  vfermltlALT  14705  modprm0  14708  modprmn0modprm0  14710  pcpremul  14745  pcmul  14753  prmdvdsprmo  14952  prmdvdsprmorOLD  14967  prmgaplem4  14976  prmgaplem7  14979  cshwsidrepsw  15016  gsmsymgreqlem2  17016  symgfixfo  17024  fsfnn0gsumfsffz  17540  irredn0  17859  rim0to0  17898  lsppratlem1  18298  ixpsnbasval  18360  cply1coe0bi  18822  dvdsrzring  18979  matinvgcell  19384  mat1dimcrng  19426  dmatscmcl  19452  scmatmats  19460  scmatscm  19462  scmatmulcl  19467  scmatghm  19482  scmatmhm  19483  ma1repvcl  19519  mdet1  19550  mdet0  19555  slesolinv  19629  slesolinvbi  19630  cramerimplem1  19632  cramerimp  19635  cramerlem1  19636  cramer  19640  cpmatacl  19664  cpmatmcl  19667  mat2pmatghm  19678  mat2pmatmul  19679  m2pmfzgsumcl  19696  decpmatmul  19720  decpmatmulsumfsupp  19721  pmatcollpwfi  19730  pmatcollpwscmat  19739  pm2mpf1  19747  pm2mpghm  19764  pm2mpmhmlem1  19766  monmat2matmon  19772  chpdmatlem2  19787  chpdmat  19789  chfacfisf  19802  cpmadugsumlemB  19822  cpmadugsumlemC  19823  cpmadugsumlemF  19824  clscld  19986  neiptopnei  20072  2ndcdisj2  20396  comppfsc  20471  tx1stc  20589  opnfbas  20781  fbasfip  20807  alexsublem  20983  alexsubALTlem4  20989  cnextcn  21006  bcthlem5  22182  vitalilem4  22443  vitalilem5  22444  itg2mulc  22579  dvcobr  22774  dvcnvlem  22802  dvferm1  22811  dvne0  22837  mdegmullem  22901  plyeq0lem  23029  plyexmo  23131  aalioulem5  23154  aalioulem6  23155  aaliou  23156  cxple2a  23506  cxpaddlelem  23553  cxpaddle  23554  relogbcxpb  23586  bcmono  24065  lgsquadlem2  24143  colinearalg  24783  axcontlem3  24839  usgraexmpl  24971  nb3grapr  25023  nb3grapr2  25024  nb3gra2nb  25025  cusgrarn  25029  cusgrasizeindslem3  25045  spthonepeq  25159  fargshiftfva  25209  wlkiswwlksur  25289  clwwlknimp  25346  clwlkisclwwlklem2a  25355  clwlkisclwwlklem0  25358  wwlksubclwwlk  25374  clwwisshclww  25377  clwwnisshclwwn  25379  eleclclwwlknlem2  25388  usg2spthonot1  25460  vdusgraval  25477  cusgraisrusgra  25508  rusgranumwlk  25527  eupatrl  25538  1to3vfriswmgra  25577  frgranbnb  25590  vdfrgra0  25592  vdgn0frgrav2  25594  vdgn1frgrav2  25596  frgrawopreg  25619  frg2wot1  25627  usg2spot2nb  25635  frgraregorufrg  25642  numclwwlkovfel2  25653  numclwlk1lem2foa  25661  numclwlk1lem2fv  25663  numclwwlk1  25668  numclwlk2lem2fv  25674  numclwwlk4  25680  numclwwlk5  25682  numclwwlk6  25683  frgrareg  25687  frgraregord013  25688  ex-natded9.20-2  25710  grpoidinvlem3  25776  grpoidinv  25778  isdivrngo  26001  sspival  26219  nmobndseqi  26262  nmobndseqiALT  26263  hvaddsub4  26563  hhcmpl  26685  ocsh  26768  5oalem2  27140  5oalem5  27143  3oalem2  27148  pjjsi  27185  hoadddir  27289  leopmul  27619  stge1i  27723  hatomistici  27847  mdsymlem2  27889  mdsymlem5  27892  addltmulALT  27931  isoun  28119  crefdf  28511  qqhre  28660  esumiun  28751  sxbrsigalem0  28929  dya2iocnei  28940  sxbrsigalem5  28946  sibfinima  28997  eulerpartlemgs2  29036  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemsup  29160  bnj529  29336  bnj945  29370  bnj1098  29380  bnj1533  29448  bnj605  29503  bnj594  29508  bnj607  29512  bnj966  29540  bnj967  29541  bnj996  29551  bnj999  29553  bnj1006  29555  bnj1118  29578  bnj1172  29595  bnj1279  29612  bnj1296  29615  bnj1498  29655  cvmsi  29773  fv2ndcnv  30207  elno2  30325  nobndlem6  30368  trisegint  30577  funtransport  30580  btwnconn1lem4  30639  btwnconn2  30651  segcon2  30654  outsideofeu  30680  isfne  30777  lukshef-ax2  30857  limsucncmpi  30887  bj-elid3  31383  bj-eldiag2  31389  poimirlem26  31670  poimirlem27  31671  poimirlem29  31673  poimirlem30  31674  poimirlem32  31676  heicant  31679  ismblfin  31685  itg2gt0cn  31701  bddiblnc  31716  areacirc  31741  opelopab3  31747  isdrngo2  31901  fldcrng  31941  flddmn  31995  cmtbr4N  32530  linepsubN  33026  pmapsub  33042  paddasslem14  33107  pclcmpatN  33175  trlval2  33438  cdleme20  33600  cdleme21j  33612  dvalveclem  34302  dia2dimlem7  34347  dvhlveclem  34385  docaclN  34401  dihjat1  34706  mapdhcl  35004  mapdh6dN  35016  mapdh8  35066  hdmap1l6d  35091  hdmap10  35120  hdmaprnlem17N  35143  hdmaplkr  35193  hdmapip0  35195  hgmapvv  35206  cmpfiiin  35248  pellexlem4  35386  pellqrex  35436  acongtr  35538  acongrep  35540  jm2.23  35561  rp-fakeanorass  35860  rp-isfinite6  35866  pm10.55  36359  refsum2cnlem1  37002  fmuldfeq  37237  climsuse  37263  limclner  37308  icccncfext  37341  stoweidlem26  37459  stoweidlem52  37486  stoweidlem57  37491  fourierdlem20  37562  fourierdlem41  37583  fourierdlem52  37594  fourierdlem64  37606  fourierdlem102  37644  fourierdlem114  37656  afvelrn  38073  opoeALTV  38215  evensumeven  38237  sgoldbalt  38285  evengpop3  38296  evengpoap3  38297  nnsum4primeseven  38298  nnsum4primesevenALTV  38299  wtgoldbnnsum4prm  38300  bgoldbnnsum3prm  38302  tgoldbach  38314  proththd  38317  ccatpfx  38353  pfxccat3  38370  pfxccatpfx2  38372  pfxccat3a  38373  reuccatpfxs1  38378  elpwdifsn  38386  lesubnn0  38412  elfz2z  38417  2ffzoeq  38426  edgssv2ALT  38484  edgssv2  38485  usgfislem2  38528  usgfisALTlem2  38532  assintop  38616  isringrng  38652  rnglz  38655  c0snmgmhm  38685  zrrnghm  38688  uzlidlring  38700  2zrngnmrid  38721  cznrng  38728  rnghmsubcsetclem2  38749  rhmsubcsetclem2  38795  rhmsubcrngclem2  38801  lmodvsmdi  38940  lincsum  38995  lincsumcl  38997  el0ldep  39032  ldepspr  39039  lindssnlvec  39052  modn0mul  39097  m1modmmod  39098  elbigolo1  39142  nn0digval  39185  aacllem  39314