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  1821  sbidm  1862  disamis  2153  r19.28v  2622  fun11uni  5324  fabexg  5441  fores  5486  f1oabexg  5512  fun11iun  5521  fvelrnb  5604  ssimaex  5618  foeqcnvco  5833  f1eqcocnv  5834  isoini  5861  brtposg  6307  tfrcllemssrecs  6405  fiintim  6985  djuex  7102  elni2  7374  dmaddpqlem  7437  nqpi  7438  ltexnqq  7468  nq0nn  7502  nqnq0a  7514  nqnq0m  7515  elnp1st2nd  7536  mullocprlem  7630  cnegexlem3  8196  divmulasscomap  8715  lediv2a  8914  btwnz  9436  eluz2b2  9668  uz2mulcl  9673  eqreznegel  9679  elioo4g  10000  fz0fzelfz0  10193  fz0fzdiffz0  10196  2ffzeq  10207  elfzodifsumelfzo  10268  elfzom1elp1fzo  10269  zpnn0elfzo  10274  ioo0  10328  zmodidfzoimp  10425  expcl2lemap  10622  iswrdsymb  10932  mulreap  11008  redivap  11018  imdivap  11025  caucvgrelemcau  11124  zproddc  11722  fprodseq  11726  p1modz1  11937  negdvdsb  11950  muldvds1  11959  muldvds2  11960  dvdsdivcl  11992  nn0ehalf  12044  nn0oddm1d2  12050  nnoddm1d2  12051  infssuzex  12086  divgcdnn  12112  coprmgcdb  12226  divgcdcoprm0  12239  pw2dvdslemn  12303  oddprmdvds  12492  4sqexercise1  12536  4sqexercise2  12537  grpissubg  13264  ecqusaddd  13308  ecqusaddcl  13309  rnglz  13441  qusmulrng  14028  quscrng  14029  dvdsrzring  14091  lgsprme0  15158  gausslemma2dlem0e  15169  gausslemma2dlem1a  15174  gausslemma2dlem6  15183