Theorem anim1i 566

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

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  sylanl1  648  sylanr1  650  disamis  2406  fores  5786  ssimaex  5913  dffv2  5921  exfo  6025  oprabv  6318  ndmovass  6436  fun11uni  6727  fabexg  6729  f1oabexg  6732  fun11iun  6733  soxp  6886  tz7.48lem  7098  tz7.49c  7103  omass  7221  oewordri  7233  omabs  7288  sbthlem9  7628  fineqvlem  7727  pssnn  7731  domunfican  7785  fiint  7789  fsuppsssupp  7837  inf1  8030  infeq5  8045  cantnfle  8081  rankuni  8272  acndom  8423  acnnum  8424  cdainflem  8562  cfcof  8645  ac6num  8850  ac6s2  8857  brdom5  8898  brdom4  8899  genpnnp  9372  lediv2a  10434  supmul1  10503  nn2ge  10556  btwnz  10962  eluz2b2  11155  uz2mulcl  11160  eqreznegel  11168  xrsupexmnf  11499  xrinfmexpnf  11500  xrsupsslem  11501  xrinfmsslem  11502  supxrun  11510  ioo0  11557  elioo4g  11588  fz0fzelfz0  11784  fz0fzdiffz0  11787  2ffzeq  11798  elfzodifsumelfzo  11863  elfzom1elp1fzo  11864  zpnn0elfzo  11869  fzonfzoufzol  11894  quoremnn0  11965  zmodidfzoimp  12008  modabs  12011  modifeq2int  12031  modaddmulmod  12035  expcl2lem  12160  ccatcl  12582  ccatval3  12586  swrdfv2  12662  swrdsbslen  12664  swrdspsleq  12665  swrd0swrd  12677  swrdccatin2  12703  swrdccatin12lem3  12706  swrdccat3  12708  swrdccat3blem  12711  swrdccatid  12713  repswccat  12748  2cshw  12772  cshweqdifid  12779  lswco  12795  repsco  12796  s4f1o  12857  ccat2s1fvwALT  12884  trclun  12932  mulre  13036  rediv  13046  imdiv  13053  resqrex  13166  caurcvg2  13582  modfsummods  13689  tanval  13945  negdvdsb  14084  muldvds1  14092  muldvds2  14093  dvdscmulr  14096  dvdsmulcr  14097  divalglem8  14142  maxprmfct  14338  modprm0  14414  modprmn0modprm0  14416  pcpremul  14451  pcmul  14459  cshwsidrepsw  14662  gsmsymgreqlem2  16655  symgfixfo  16663  fsfnn0gsumfsffz  17206  irredn0  17547  rim0to0  17586  lsppratlem1  17988  ixpsnbasval  18050  cply1coe0bi  18537  dvdsrzring  18696  matinvgcell  19104  mat1dimcrng  19146  dmatscmcl  19172  scmatmats  19180  scmatscm  19182  scmatmulcl  19187  scmatghm  19202  scmatmhm  19203  ma1repvcl  19239  mdet1  19270  mdet0  19275  slesolinv  19349  slesolinvbi  19350  cramerimplem1  19352  cramerimp  19355  cramerlem1  19356  cramer  19360  cpmatacl  19384  cpmatmcl  19387  mat2pmatghm  19398  mat2pmatmul  19399  m2pmfzgsumcl  19416  decpmatmul  19440  decpmatmulsumfsupp  19441  pmatcollpwfi  19450  pmatcollpwscmat  19459  pm2mpf1  19467  pm2mpghm  19484  pm2mpmhmlem1  19486  monmat2matmon  19492  chpdmatlem2  19507  chpdmat  19509  chfacfisf  19522  cpmadugsumlemB  19542  cpmadugsumlemC  19543  cpmadugsumlemF  19544  clscld  19715  neiptopnei  19800  2ndcdisj2  20124  comppfsc  20199  tx1stc  20317  opnfbas  20509  fbasfip  20535  alexsublem  20710  alexsubALTlem4  20716  cnextcn  20733  bcthlem5  21933  vitalilem4  22186  vitalilem5  22187  itg2mulc  22320  dvcobr  22515  dvcnvlem  22543  dvferm1  22552  dvne0  22578  mdegmullem  22644  plyeq0lem  22773  plyexmo  22875  aalioulem5  22898  aalioulem6  22899  aaliou  22900  cxple2a  23248  cxpaddlelem  23293  cxpaddle  23294  relogbcxpb  23326  bcmono  23750  lgsquadlem2  23828  colinearalg  24415  axcontlem3  24471  usgraexmpl  24603  nb3grapr  24655  nb3grapr2  24656  nb3gra2nb  24657  cusgrarn  24661  cusgrasizeindslem3  24677  spthonepeq  24791  fargshiftfva  24841  wlkiswwlksur  24921  clwwlknimp  24978  clwlkisclwwlklem2a  24987  clwlkisclwwlklem0  24990  wwlksubclwwlk  25006  clwwisshclww  25009  clwwnisshclwwn  25011  eleclclwwlknlem2  25020  usg2spthonot1  25092  vdusgraval  25109  cusgraisrusgra  25140  rusgranumwlk  25159  eupatrl  25170  1to3vfriswmgra  25209  frgranbnb  25222  vdfrgra0  25224  vdgn0frgrav2  25226  vdgn1frgrav2  25228  frgrawopreg  25251  frg2wot1  25259  usg2spot2nb  25267  frgraregorufrg  25274  numclwwlkovfel2  25285  numclwlk1lem2foa  25293  numclwlk1lem2fv  25295  numclwwlk1  25300  numclwlk2lem2fv  25306  numclwwlk4  25312  numclwwlk5  25314  numclwwlk6  25315  frgrareg  25319  frgraregord013  25320  ex-natded9.20-2  25341  grpoidinvlem3  25406  grpoidinv  25408  isdivrngo  25631  sspival  25849  nmobndseqi  25892  nmobndseqiALT  25893  hvaddsub4  26193  hhcmpl  26315  ocsh  26399  5oalem2  26771  5oalem5  26774  3oalem2  26779  pjjsi  26816  hoadddir  26921  leopmul  27251  stge1i  27355  hatomistici  27479  mdsymlem2  27521  mdsymlem5  27524  addltmulALT  27563  isoun  27748  crefdf  28086  qqhre  28232  esumiun  28323  sxbrsigalem0  28479  dya2iocnei  28490  sxbrsigalem5  28496  sibfinima  28545  eulerpartlemgs2  28583  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemsup  28707  cvmsi  28974  elno2  29654  nobndlem6  29697  trisegint  29906  funtransport  29909  btwnconn1lem4  29968  btwnconn2  29980  segcon2  29983  outsideofeu  30009  lukshef-ax2  30108  limsucncmpi  30138  heicant  30289  ismblfin  30295  itg2gt0cn  30310  bddiblnc  30325  areacirc  30352  isfne  30397  opelopab3  30447  isdrngo2  30601  fldcrng  30641  flddmn  30695  cmpfiiin  30869  pellexlem4  31007  pellqrex  31054  acongtr  31155  acongrep  31157  jm2.23  31177  pm10.55  31515  refsum2cnlem1  31652  fmuldfeq  31816  climsuse  31853  limclner  31896  icccncfext  31929  stoweidlem26  32047  stoweidlem52  32073  stoweidlem57  32078  fourierdlem20  32148  fourierdlem41  32169  fourierdlem52  32180  fourierdlem64  32192  fourierdlem102  32230  fourierdlem114  32242  afvelrn  32492  opoeALTV  32589  ccatpfx  32637  pfxccat3  32654  pfxccatpfx2  32656  pfxccat3a  32657  reuccatpfxs1  32662  elpwdifsn  32670  lesubnn0  32700  elfz2z  32705  2ffzoeq  32715  edgssv2ALT  32773  edgssv2  32774  usgfislem2  32817  usgfisALTlem2  32821  assintop  32905  isringrng  32941  rnglz  32944  c0snmgmhm  32974  zrrnghm  32977  uzlidlring  32989  2zrngnmrid  33010  cznrng  33017  rnghmsubcsetclem2  33038  rhmsubcsetclem2  33084  rhmsubcrngclem2  33090  lmodvsmdi  33229  lincsum  33284  lincsumcl  33286  el0ldep  33321  ldepspr  33328  lindssnlvec  33341  modn0mul  33387  m1modmmod  33388  elbigolo1  33432  nn0digval  33475  aacllem  33604  bnj529  34199  bnj945  34233  bnj1098  34243  bnj1533  34311  bnj605  34366  bnj594  34371  bnj607  34375  bnj966  34403  bnj967  34404  bnj996  34414  bnj999  34416  bnj1006  34418  bnj1118  34441  bnj1172  34458  bnj1279  34475  bnj1296  34478  bnj1498  34518  bj-elid3  35002  bj-eldiag2  35008  cmtbr4N  35377  linepsubN  35873  pmapsub  35889  paddasslem14  35954  pclcmpatN  36022  trlval2  36285  cdleme20  36447  cdleme21j  36459  dvalveclem  37149  dia2dimlem7  37194  dvhlveclem  37232  docaclN  37248  dihjat1  37553  mapdhcl  37851  mapdh6dN  37863  mapdh8  37913  hdmap1l6d  37938  hdmap10  37967  hdmaprnlem17N  37990  hdmaplkr  38040  hdmapip0  38042  hgmapvv  38053  rp-fakeanorass  38151  rp-isfinite6  38157