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  5328  fabexg  5445  fores  5490  f1oabexg  5516  fun11iun  5525  fvelrnb  5608  ssimaex  5622  foeqcnvco  5837  f1eqcocnv  5838  isoini  5865  brtposg  6312  tfrcllemssrecs  6410  fiintim  6992  djuex  7109  elni2  7381  dmaddpqlem  7444  nqpi  7445  ltexnqq  7475  nq0nn  7509  nqnq0a  7521  nqnq0m  7522  elnp1st2nd  7543  mullocprlem  7637  cnegexlem3  8203  divmulasscomap  8723  lediv2a  8922  btwnz  9445  eluz2b2  9677  uz2mulcl  9682  eqreznegel  9688  elioo4g  10009  fz0fzelfz0  10202  fz0fzdiffz0  10205  2ffzeq  10216  elfzodifsumelfzo  10277  elfzom1elp1fzo  10278  zpnn0elfzo  10283  infssuzex  10323  ioo0  10349  zmodidfzoimp  10446  expcl2lemap  10643  iswrdsymb  10953  mulreap  11029  redivap  11039  imdivap  11046  caucvgrelemcau  11145  zproddc  11744  fprodseq  11748  p1modz1  11959  negdvdsb  11972  muldvds1  11981  muldvds2  11982  dvdsdivcl  12015  nn0ehalf  12068  nn0oddm1d2  12074  nnoddm1d2  12075  divgcdnn  12142  coprmgcdb  12256  divgcdcoprm0  12269  pw2dvdslemn  12333  oddprmdvds  12523  4sqexercise1  12567  4sqexercise2  12568  grpissubg  13324  ecqusaddd  13368  ecqusaddcl  13369  rnglz  13501  qusmulrng  14088  quscrng  14089  dvdsrzring  14159  lgsprme0  15283  gausslemma2dlem0e  15294  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  lgsquadlem2  15319  2lgsoddprm  15354