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  1824  sbidm  1865  disamis  2156  r19.28v  2625  fun11uni  5329  fabexg  5448  fores  5493  f1oabexg  5519  fun11iun  5528  fvelrnb  5611  ssimaex  5625  foeqcnvco  5840  f1eqcocnv  5841  isoini  5868  brtposg  6321  tfrcllemssrecs  6419  fiintim  7001  djuex  7118  elni2  7398  dmaddpqlem  7461  nqpi  7462  ltexnqq  7492  nq0nn  7526  nqnq0a  7538  nqnq0m  7539  elnp1st2nd  7560  mullocprlem  7654  cnegexlem3  8220  divmulasscomap  8740  lediv2a  8939  btwnz  9462  eluz2b2  9694  uz2mulcl  9699  eqreznegel  9705  elioo4g  10026  fz0fzelfz0  10219  fz0fzdiffz0  10222  2ffzeq  10233  elfzodifsumelfzo  10294  elfzom1elp1fzo  10295  zpnn0elfzo  10300  infssuzex  10340  ioo0  10366  zmodidfzoimp  10463  expcl2lemap  10660  iswrdsymb  10970  mulreap  11046  redivap  11056  imdivap  11063  caucvgrelemcau  11162  zproddc  11761  fprodseq  11765  p1modz1  11976  negdvdsb  11989  muldvds1  11998  muldvds2  11999  dvdsdivcl  12032  nn0ehalf  12085  nn0oddm1d2  12091  nnoddm1d2  12092  divgcdnn  12167  coprmgcdb  12281  divgcdcoprm0  12294  pw2dvdslemn  12358  oddprmdvds  12548  4sqexercise1  12592  4sqexercise2  12593  grpissubg  13400  ecqusaddd  13444  ecqusaddcl  13445  rnglz  13577  qusmulrng  14164  quscrng  14165  dvdsrzring  14235  lgsprme0  15367  gausslemma2dlem0e  15378  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  lgsquadlem2  15403  2lgsoddprm  15438