Theorem anim1i 552

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  sylanl1  632  sylanr1  634  disamis  2364  ordelinel  4639  fun11uni  5478  fabexg  5583  fores  5621  f1oabexg  5645  fun11iun  5654  ssimaex  5747  dffv2  5755  exfo  5846  ndmovass  6194  soxp  6418  tz7.48lem  6657  tz7.49c  6662  omass  6782  oewordri  6794  omabs  6849  sbthlem9  7184  fineqvlem  7282  pssnn  7286  domunfican  7338  fiint  7342  inf1  7533  infeq5  7548  rankuni  7745  acndom  7888  acnnum  7889  cdainflem  8027  cfcof  8110  ac6num  8315  ac6s2  8322  brdom5  8363  brdom4  8364  genpnnp  8838  lediv2a  9860  supmul1  9929  nn2ge  9981  btwnz  10328  eluz2b2  10504  uz2mulcl  10509  eqreznegel  10517  xrsupexmnf  10839  xrinfmexpnf  10840  xrsupsslem  10841  xrinfmsslem  10842  supxrun  10850  ioo0  10897  elioo4g  10927  quoremnn0  11192  modabs  11229  expcl2lem  11348  s4f1o  11820  mulre  11881  rediv  11891  imdiv  11898  resqrex  12011  caurcvg2  12426  tanval  12684  negdvdsb  12821  muldvds1  12829  muldvds2  12830  dvdscmulr  12833  dvdsmulcr  12834  divalglem8  12875  maxprmfct  13068  pcpremul  13172  pcmul  13180  irredn0  15763  lsppratlem1  16174  dvdsrz  16722  clscld  17066  neiptopnei  17151  2ndcdisj2  17473  tx1stc  17635  opnfbas  17827  fbasfip  17853  alexsublem  18028  alexsubALTlem4  18034  cnextcn  18051  bcthlem5  19234  vitalilem4  19456  vitalilem5  19457  itg2mulc  19592  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq3  19602  itg2addlem  19603  itg2gt0  19605  itg2cnlem2  19607  dvcobr  19785  dvcnvlem  19813  dvferm1  19822  dvne0  19848  mdegmullem  19954  plyeq0lem  20082  plyexmo  20183  aalioulem5  20206  aalioulem6  20207  aaliou  20208  cxple2a  20543  cxpaddlelem  20588  cxpaddle  20589  bcmono  21014  lgsquadlem2  21092  usgraexmpl  21373  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgrarn  21421  cusgrasizeindslem3  21437  spthonepeq  21540  fargshiftfva  21579  vdusgraval  21631  eupatrl  21643  ex-natded9.20-2  21679  grpoidinvlem3  21747  grpoidinv  21749  ablomul  21896  isdivrngo  21972  sspival  22190  nmobndseqi  22233  nmobndseqiOLD  22234  hvaddsub4  22533  hhcmpl  22655  ocsh  22738  5oalem2  23110  5oalem5  23113  3oalem2  23118  pjjsi  23155  hoadddir  23260  leopmul  23590  stge1i  23694  hatomistici  23818  mdsymlem2  23860  mdsymlem5  23863  addltmulALT  23902  isoun  24042  qqhre  24339  sxbrsigalem0  24574  dya2iocnei  24585  sxbrsigalem5  24591  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsup  24715  cvmsi  24905  elno2  25522  nobndlem6  25565  colinearalg  25753  axcontlem3  25809  trisegint  25866  funtransport  25869  btwnconn1lem4  25928  btwnconn2  25940  segcon2  25943  outsideofeu  25969  lukshef-ax2  26069  limsucncmpi  26099  ismblfin  26146  itg2addnc  26158  itg2gt0cn  26159  bddiblnc  26174  areacirc  26187  isfne  26238  comppfsc  26277  opelopab3  26308  isdrngo2  26464  fldcrng  26504  flddmn  26558  cmpfiiin  26641  pellexlem4  26785  pellqrex  26832  acongtr  26933  acongrep  26935  jm2.23  26957  pm10.55  27432  refsum2cnlem1  27575  fmuldfeq  27580  climsuse  27601  stoweidlem26  27642  stoweidlem52  27668  stoweidlem57  27673  afvelrn  27899  lesubnn0  27972  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccat3  28029  usg2spthonot1  28087  1to3vfriswmgra  28111  frgranbnb  28124  vdfrgra0  28126  vdgfrgra0  28127  vdgn0frgrav2  28129  vdgn1frgrav2  28131  frgrawopreg  28152  frg2wot1  28160  usg2spot2nb  28168  bnj529  28815  bnj945  28850  bnj1098  28860  bnj1533  28929  bnj605  28984  bnj594  28989  bnj607  28993  bnj966  29021  bnj967  29022  bnj996  29032  bnj999  29034  bnj1006  29036  bnj1118  29059  bnj1172  29076  bnj1279  29093  bnj1296  29096  bnj1498  29136  cmtbr4N  29738  linepsubN  30234  pmapsub  30250  paddasslem14  30315  pclcmpatN  30383  trlval2  30645  cdleme20  30806  cdleme21j  30818  dvalveclem  31508  dia2dimlem7  31553  dvhlveclem  31591  docaclN  31607  dihjat1  31912  mapdhcl  32210  mapdh6dN  32222  mapdh8  32272  hdmap1l6d  32297  hdmap10  32326  hdmaprnlem17N  32349  hdmaplkr  32399  hdmapip0  32401  hgmapvv  32412

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361