Theorem anim1i 340

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanl1  402  sylanr1  404  mpan10  474  sbcof2  1856  sbidm  1897  disamis  2189  r19.28v  2659  fun11uni  5391  fabexg  5515  fores  5560  f1oabexg  5586  fun11iun  5595  fdmeu  5679  fvelrnb  5683  ssimaex  5697  foeqcnvco  5920  f1eqcocnv  5921  isoini  5948  brtposg  6406  tfrcllemssrecs  6504  fiintim  7104  djuex  7221  elni2  7512  dmaddpqlem  7575  nqpi  7576  ltexnqq  7606  nq0nn  7640  nqnq0a  7652  nqnq0m  7653  elnp1st2nd  7674  mullocprlem  7768  cnegexlem3  8334  divmulasscomap  8854  lediv2a  9053  btwnz  9577  eluz2b2  9810  uz2mulcl  9815  eqreznegel  9821  elioo4g  10142  fz0fzelfz0  10335  fz0fzdiffz0  10338  2ffzeq  10349  elfzodifsumelfzo  10419  elfzom1elp1fzo  10420  zpnn0elfzo  10425  infssuzex  10465  ioo0  10491  zmodidfzoimp  10588  expcl2lemap  10785  iswrdsymb  11102  ccatcl  11141  ccatsymb  11150  swrdfv2  11210  swrdsbslen  11213  swrdspsleq  11214  pfxswrd  11253  pfxccatin12lem3  11279  pfxccatpfx2  11284  swrdccat3blem  11286  reuccatpfxs1  11294  mulreap  11390  redivap  11400  imdivap  11407  caucvgrelemcau  11506  zproddc  12105  fprodseq  12109  p1modz1  12320  negdvdsb  12333  muldvds1  12342  muldvds2  12343  dvdsdivcl  12376  nn0ehalf  12429  nn0oddm1d2  12435  nnoddm1d2  12436  divgcdnn  12511  coprmgcdb  12625  divgcdcoprm0  12638  pw2dvdslemn  12702  oddprmdvds  12892  4sqexercise1  12936  4sqexercise2  12937  grpissubg  13746  ecqusaddd  13790  ecqusaddcl  13791  rnglz  13923  qusmulrng  14511  quscrng  14512  dvdsrzring  14582  lgsprme0  15736  gausslemma2dlem0e  15747  gausslemma2dlem1a  15752  gausslemma2dlem6  15761  lgsquadlem2  15772  2lgsoddprm  15807  usgrislfuspgrdom  16003  edgssv2en  16012  umgr2edg  16020  uspgredg2v  16034  vtxdfifiun  16056