Theorem anim1i 578

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

Syntax hints:   -> wi 4   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  sylanl1  662  sylanr1  664  disamis  2425  fores  5815  ssimaex  5945  dffv2  5953  exfo  6055  frnssb  6067  oprabv  6358  ndmovass  6476  fun11uni  6766  fabexg  6768  f1oabexg  6771  fun11iun  6772  soxp  6928  tz7.48lem  7176  tz7.49c  7181  omass  7299  oewordri  7311  omabs  7366  sbthlem9  7708  fineqvlem  7804  pssnn  7808  domunfican  7862  fiint  7866  fsuppsssupp  7917  sup0  7998  inf1  8145  infeq5  8160  cantnfle  8194  rankuni  8352  acndom  8500  acnnum  8501  cdainflem  8639  cfcof  8722  ac6num  8927  ac6s2  8934  brdom5  8975  brdom4  8976  genpnnp  9448  lediv2a  10522  supmul1  10598  infregelb  10616  nn2ge  10656  btwnz  11060  eluz2b2  11254  uz2mulcl  11259  eqreznegel  11272  xrsupexmnf  11615  xrinfmexpnf  11616  xrsupsslem  11617  xrinfmsslem  11618  supxrun  11626  ioo0  11686  elioo4g  11720  fz0fzelfz0  11922  fz0fzdiffz0  11925  2ffzeq  11937  elfzodifsumelfzo  12009  elfzom1elp1fzo  12010  zpnn0elfzo  12015  elfzom1elp1fzo1  12040  fzonfzoufzol  12043  quoremnn0  12116  zmodidfzoimp  12160  modabs  12163  modifeq2int  12186  modaddmulmod  12190  expcl2lem  12322  iswrdsymb  12735  ccatcl  12771  ccatval3  12775  ccatalpha  12787  swrdfv2  12856  swrdsbslen  12858  swrdspsleq  12859  swrd0swrd  12871  swrdccatin2  12897  swrdccatin12lem3  12900  swrdccat3  12902  swrdccat3blem  12905  swrdccatid  12907  repswccat  12942  2cshw  12969  cshweqdifid  12976  lswco  12994  repsco  12995  s4f1o  13072  ccat2s1fvwALT  13105  trclun  13155  mulre  13261  rediv  13271  imdiv  13278  resqrex  13391  caurcvg2  13821  modfsummods  13930  tanval  14259  negdvdsb  14396  muldvds1  14404  muldvds2  14405  dvdscmulr  14408  dvdsmulcr  14409  divalglem8  14459  lcmfunsnlem2lem2  14691  lcmfun  14697  maxprmfct  14731  coprmgcdb  14733  ncoprmgcdne1b  14734  ncoprmlnprm  14756  vfermltl  14831  vfermltlALT  14832  modprm0  14835  modprmn0modprm0  14837  pcpremul  14872  pcmul  14880  prmdvdsprmo  15079  prmdvdsprmorOLD  15094  prmgaplem4  15103  prmgaplem7  15106  cshwsidrepsw  15142  gsmsymgreqlem2  17150  symgfixfo  17158  fsfnn0gsumfsffz  17690  irredn0  18009  rim0to0  18048  lsppratlem1  18448  ixpsnbasval  18510  cply1coe0bi  18971  dvdsrzring  19129  matinvgcell  19537  mat1dimcrng  19579  dmatscmcl  19605  scmatmats  19613  scmatscm  19615  scmatmulcl  19620  scmatghm  19635  scmatmhm  19636  ma1repvcl  19672  mdet1  19703  mdet0  19708  slesolinv  19782  slesolinvbi  19783  cramerimplem1  19785  cramerimp  19788  cramerlem1  19789  cramer  19793  cpmatacl  19817  cpmatmcl  19820  mat2pmatghm  19831  mat2pmatmul  19832  m2pmfzgsumcl  19849  decpmatmul  19873  decpmatmulsumfsupp  19874  pmatcollpwfi  19883  pmatcollpwscmat  19892  pm2mpf1  19900  pm2mpghm  19917  pm2mpmhmlem1  19919  monmat2matmon  19925  chpdmatlem2  19940  chpdmat  19942  chfacfisf  19955  cpmadugsumlemB  19975  cpmadugsumlemC  19976  cpmadugsumlemF  19977  clscld  20139  neiptopnei  20225  2ndcdisj2  20549  comppfsc  20624  tx1stc  20742  opnfbas  20935  fbasfip  20961  alexsublem  21137  alexsubALTlem4  21143  cnextcn  21160  bcthlem5  22374  vitalilem4  22648  vitalilem5  22649  itg2mulc  22784  dvcobr  22979  dvcnvlem  23007  dvferm1  23016  dvne0  23042  mdegmullem  23106  plyeq0lem  23243  plyexmo  23345  aalioulem5  23371  aalioulem6  23372  aaliou  23373  cxple2a  23723  cxpaddlelem  23770  cxpaddle  23771  relogbcxpb  23803  bcmono  24284  lgsquadlem2  24362  colinearalg  25019  axcontlem3  25075  usgraexmplef  25207  nb3grapr  25260  nb3grapr2  25261  nb3gra2nb  25262  cusgrarn  25266  cusgrasizeindslem3  25282  spthonepeq  25396  fargshiftfva  25446  wlkiswwlksur  25526  clwwlknimp  25583  clwlkisclwwlklem2a  25592  clwlkisclwwlklem0  25595  wwlksubclwwlk  25611  clwwisshclww  25614  clwwnisshclwwn  25616  eleclclwwlknlem2  25625  usg2spthonot1  25697  vdusgraval  25714  cusgraisrusgra  25745  rusgranumwlk  25764  eupatrl  25775  1to3vfriswmgra  25814  frgranbnb  25827  vdfrgra0  25829  vdgn0frgrav2  25831  vdgn1frgrav2  25833  frgrawopreg  25856  frg2wot1  25864  usg2spot2nb  25872  frgraregorufrg  25879  numclwwlkovfel2  25890  numclwlk1lem2foa  25898  numclwlk1lem2fv  25900  numclwwlk1  25905  numclwlk2lem2fv  25911  numclwwlk4  25917  numclwwlk5  25919  numclwwlk6  25920  frgrareg  25924  frgraregord013  25925  ex-natded9.20-2  25947  grpoidinvlem3  26015  grpoidinv  26017  isdivrngo  26240  sspival  26458  nmobndseqi  26501  nmobndseqiALT  26502  hvaddsub4  26812  hhcmpl  26934  ocsh  27017  5oalem2  27389  5oalem5  27392  3oalem2  27397  pjjsi  27434  hoadddir  27538  leopmul  27868  stge1i  27972  hatomistici  28096  mdsymlem2  28138  mdsymlem5  28141  addltmulALT  28180  isoun  28357  crefdf  28749  qqhre  28898  esumiun  28989  sxbrsigalem0  29166  dya2iocnei  29177  sxbrsigalem5  29183  sibfinima  29245  eulerpartlemgs2  29286  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemsup  29410  ballotlemsupOLD  29448  bnj529  29623  bnj945  29657  bnj1098  29667  bnj1533  29735  bnj605  29790  bnj594  29795  bnj607  29799  bnj966  29827  bnj967  29828  bnj996  29838  bnj999  29840  bnj1006  29842  bnj1118  29865  bnj1172  29882  bnj1279  29899  bnj1296  29902  bnj1498  29942  cvmsi  30060  fv2ndcnv  30494  elno2  30612  nobndlem6  30657  trisegint  30866  funtransport  30869  btwnconn1lem4  30928  btwnconn2  30940  segcon2  30943  outsideofeu  30969  isfne  31066  lukshef-ax2  31146  limsucncmpi  31176  bj-elid3  31712  bj-eldiag2  31717  poimirlem26  32030  poimirlem27  32031  poimirlem29  32033  poimirlem30  32034  poimirlem32  32036  heicant  32039  ismblfin  32045  itg2gt0cn  32061  bddiblnc  32076  areacirc  32101  opelopab3  32107  isdrngo2  32261  fldcrng  32301  flddmn  32355  cmtbr4N  32892  linepsubN  33388  pmapsub  33404  paddasslem14  33469  pclcmpatN  33537  trlval2  33800  cdleme20  33962  cdleme21j  33974  dvalveclem  34664  dia2dimlem7  34709  dvhlveclem  34747  docaclN  34763  dihjat1  35068  mapdhcl  35366  mapdh6dN  35378  mapdh8  35428  hdmap1l6d  35453  hdmap10  35482  hdmaprnlem17N  35505  hdmaplkr  35555  hdmapip0  35557  hgmapvv  35568  cmpfiiin  35610  pellexlem4  35747  pellqrex  35797  acongtr  35899  acongrep  35901  jm2.23  35922  rp-fakeanorass  36228  rp-isfinite6  36234  inintabss  36255  pm10.55  36788  refsum2cnlem1  37421  fmuldfeq  37758  climsuse  37784  limclner  37829  icccncfext  37862  stoweidlem26  37998  stoweidlem52  38025  stoweidlem57  38030  fourierdlem20  38101  fourierdlem41  38123  fourierdlem52  38134  fourierdlem64  38146  fourierdlem102  38184  fourierdlem114  38196  ovolval4lem1  38589  afvelrn  38815  opoeALTV  38957  evensumeven  38979  sgoldbalt  39027  evengpop3  39038  evengpoap3  39039  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  tgoldbach  39056  proththd  39059  ccatpfx  39097  pfxccat3  39114  pfxccatpfx2  39116  pfxccat3a  39117  reuccatpfxs1  39122  elpwdifsn  39137  fpropnf1  39182  lesubnn0  39195  elfz2z  39200  2ffzoeq  39209  umgrislfupgrlem  39367  edgupgr  39386  usgruspgrb  39429  usgrislfuspgr  39432  edgassv2  39443  umgr2edg  39454  usgr2edg  39455  uspgredg2v  39465  subupgr  39523  subusgr  39525  usgrfilem  39557  nbupgrres  39602  nb3gr2nb  39622  nbupgruvtxres  39644  cplgr3v  39667  cusgrres  39674  cusgrsizeindslem  39677  cusgrsizeinds  39678  vtxdun  39704  cusgrrusgr  39786  wlkOnprop  39856  1wlkreslem  39865  trlsonprop  39903  pthsonprop  39936  spthonprop  39937  spthonepeq-av  39944  uhgr1wlkspth  39947  usgr2wlkspth  39951  crctcsh1wlkn0lem6  39993  crctcsh1wlkn0lem7  39994  crctcshtrl  40001  crctcsh  40002  umgr2adedgwlkonALT  40069  uhgr3cyclex  40096  eupth2lem3lem3  40142  eucrctshift  40155  eucrct2eupth1  40156  edgssv2ALT  40221  edgssv2  40222  usgfislem2  40265  usgfisALTlem2  40269  assintop  40353  isringrng  40389  rnglz  40392  c0snmgmhm  40422  zrrnghm  40425  uzlidlring  40437  2zrngnmrid  40458  cznrng  40465  rnghmsubcsetclem2  40486  rhmsubcsetclem2  40532  rhmsubcrngclem2  40538  lmodvsmdi  40675  lincsum  40730  lincsumcl  40732  el0ldep  40767  ldepspr  40774  lindssnlvec  40787  modn0mul  40831  m1modmmod  40832  elbigolo1  40876  nn0digval  40919  aacllem  41046