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  1834  sbidm  1875  disamis  2167  r19.28v  2636  fun11uni  5363  fabexg  5485  fores  5530  f1oabexg  5556  fun11iun  5565  fvelrnb  5649  ssimaex  5663  foeqcnvco  5882  f1eqcocnv  5883  isoini  5910  brtposg  6363  tfrcllemssrecs  6461  fiintim  7054  djuex  7171  elni2  7462  dmaddpqlem  7525  nqpi  7526  ltexnqq  7556  nq0nn  7590  nqnq0a  7602  nqnq0m  7603  elnp1st2nd  7624  mullocprlem  7718  cnegexlem3  8284  divmulasscomap  8804  lediv2a  9003  btwnz  9527  eluz2b2  9759  uz2mulcl  9764  eqreznegel  9770  elioo4g  10091  fz0fzelfz0  10284  fz0fzdiffz0  10287  2ffzeq  10298  elfzodifsumelfzo  10367  elfzom1elp1fzo  10368  zpnn0elfzo  10373  infssuzex  10413  ioo0  10439  zmodidfzoimp  10536  expcl2lemap  10733  iswrdsymb  11049  ccatcl  11087  ccatsymb  11096  swrdfv2  11154  swrdsbslen  11157  swrdspsleq  11158  pfxswrd  11197  pfxccatin12lem3  11223  pfxccatpfx2  11228  swrdccat3blem  11230  reuccatpfxs1  11238  mulreap  11290  redivap  11300  imdivap  11307  caucvgrelemcau  11406  zproddc  12005  fprodseq  12009  p1modz1  12220  negdvdsb  12233  muldvds1  12242  muldvds2  12243  dvdsdivcl  12276  nn0ehalf  12329  nn0oddm1d2  12335  nnoddm1d2  12336  divgcdnn  12411  coprmgcdb  12525  divgcdcoprm0  12538  pw2dvdslemn  12602  oddprmdvds  12792  4sqexercise1  12836  4sqexercise2  12837  grpissubg  13645  ecqusaddd  13689  ecqusaddcl  13690  rnglz  13822  qusmulrng  14409  quscrng  14410  dvdsrzring  14480  lgsprme0  15634  gausslemma2dlem0e  15645  gausslemma2dlem1a  15650  gausslemma2dlem6  15659  lgsquadlem2  15670  2lgsoddprm  15705