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  1856  sbidm  1897  disamis  2189  r19.28v  2659  fun11uni  5390  fabexg  5512  fores  5557  f1oabexg  5583  fun11iun  5592  fdmeu  5676  fvelrnb  5680  ssimaex  5694  foeqcnvco  5913  f1eqcocnv  5914  isoini  5941  brtposg  6398  tfrcllemssrecs  6496  fiintim  7089  djuex  7206  elni2  7497  dmaddpqlem  7560  nqpi  7561  ltexnqq  7591  nq0nn  7625  nqnq0a  7637  nqnq0m  7638  elnp1st2nd  7659  mullocprlem  7753  cnegexlem3  8319  divmulasscomap  8839  lediv2a  9038  btwnz  9562  eluz2b2  9794  uz2mulcl  9799  eqreznegel  9805  elioo4g  10126  fz0fzelfz0  10319  fz0fzdiffz0  10322  2ffzeq  10333  elfzodifsumelfzo  10402  elfzom1elp1fzo  10403  zpnn0elfzo  10408  infssuzex  10448  ioo0  10474  zmodidfzoimp  10571  expcl2lemap  10768  iswrdsymb  11084  ccatcl  11123  ccatsymb  11132  swrdfv2  11190  swrdsbslen  11193  swrdspsleq  11194  pfxswrd  11233  pfxccatin12lem3  11259  pfxccatpfx2  11264  swrdccat3blem  11266  reuccatpfxs1  11274  mulreap  11370  redivap  11380  imdivap  11387  caucvgrelemcau  11486  zproddc  12085  fprodseq  12089  p1modz1  12300  negdvdsb  12313  muldvds1  12322  muldvds2  12323  dvdsdivcl  12356  nn0ehalf  12409  nn0oddm1d2  12415  nnoddm1d2  12416  divgcdnn  12491  coprmgcdb  12605  divgcdcoprm0  12618  pw2dvdslemn  12682  oddprmdvds  12872  4sqexercise1  12916  4sqexercise2  12917  grpissubg  13726  ecqusaddd  13770  ecqusaddcl  13771  rnglz  13903  qusmulrng  14490  quscrng  14491  dvdsrzring  14561  lgsprme0  15715  gausslemma2dlem0e  15726  gausslemma2dlem1a  15731  gausslemma2dlem6  15740  lgsquadlem2  15751  2lgsoddprm  15786  usgrislfuspgrdom  15982  edgssv2en  15991  umgr2edg  15999  uspgredg2v  16013