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  1833  sbidm  1874  disamis  2165  r19.28v  2634  fun11uni  5344  fabexg  5463  fores  5508  f1oabexg  5534  fun11iun  5543  fvelrnb  5626  ssimaex  5640  foeqcnvco  5859  f1eqcocnv  5860  isoini  5887  brtposg  6340  tfrcllemssrecs  6438  fiintim  7028  djuex  7145  elni2  7427  dmaddpqlem  7490  nqpi  7491  ltexnqq  7521  nq0nn  7555  nqnq0a  7567  nqnq0m  7568  elnp1st2nd  7589  mullocprlem  7683  cnegexlem3  8249  divmulasscomap  8769  lediv2a  8968  btwnz  9492  eluz2b2  9724  uz2mulcl  9729  eqreznegel  9735  elioo4g  10056  fz0fzelfz0  10249  fz0fzdiffz0  10252  2ffzeq  10263  elfzodifsumelfzo  10330  elfzom1elp1fzo  10331  zpnn0elfzo  10336  infssuzex  10376  ioo0  10402  zmodidfzoimp  10499  expcl2lemap  10696  iswrdsymb  11012  ccatcl  11049  ccatsymb  11058  swrdfv2  11116  swrdsbslen  11119  swrdspsleq  11120  mulreap  11175  redivap  11185  imdivap  11192  caucvgrelemcau  11291  zproddc  11890  fprodseq  11894  p1modz1  12105  negdvdsb  12118  muldvds1  12127  muldvds2  12128  dvdsdivcl  12161  nn0ehalf  12214  nn0oddm1d2  12220  nnoddm1d2  12221  divgcdnn  12296  coprmgcdb  12410  divgcdcoprm0  12423  pw2dvdslemn  12487  oddprmdvds  12677  4sqexercise1  12721  4sqexercise2  12722  grpissubg  13530  ecqusaddd  13574  ecqusaddcl  13575  rnglz  13707  qusmulrng  14294  quscrng  14295  dvdsrzring  14365  lgsprme0  15519  gausslemma2dlem0e  15530  gausslemma2dlem1a  15535  gausslemma2dlem6  15544  lgsquadlem2  15555  2lgsoddprm  15590