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  5397  fabexg  5521  fores  5566  f1oabexg  5592  fun11iun  5601  fdmeu  5685  fvelrnb  5689  ssimaex  5703  foeqcnvco  5926  f1eqcocnv  5927  isoini  5954  brtposg  6415  tfrcllemssrecs  6513  fiintim  7116  djuex  7233  elni2  7524  dmaddpqlem  7587  nqpi  7588  ltexnqq  7618  nq0nn  7652  nqnq0a  7664  nqnq0m  7665  elnp1st2nd  7686  mullocprlem  7780  cnegexlem3  8346  divmulasscomap  8866  lediv2a  9065  btwnz  9589  eluz2b2  9827  uz2mulcl  9832  eqreznegel  9838  elioo4g  10159  fz0fzelfz0  10352  fz0fzdiffz0  10355  2ffzeq  10366  elfzodifsumelfzo  10436  elfzom1elp1fzo  10437  zpnn0elfzo  10442  infssuzex  10483  ioo0  10509  zmodidfzoimp  10606  expcl2lemap  10803  iswrdsymb  11121  ccatcl  11160  ccatsymb  11169  swrdfv2  11234  swrdsbslen  11237  swrdspsleq  11238  pfxswrd  11277  pfxccatin12lem3  11303  pfxccatpfx2  11308  swrdccat3blem  11310  reuccatpfxs1  11318  mulreap  11415  redivap  11425  imdivap  11432  caucvgrelemcau  11531  zproddc  12130  fprodseq  12134  p1modz1  12345  negdvdsb  12358  muldvds1  12367  muldvds2  12368  dvdsdivcl  12401  nn0ehalf  12454  nn0oddm1d2  12460  nnoddm1d2  12461  divgcdnn  12536  coprmgcdb  12650  divgcdcoprm0  12663  pw2dvdslemn  12727  oddprmdvds  12917  4sqexercise1  12961  4sqexercise2  12962  grpissubg  13771  ecqusaddd  13815  ecqusaddcl  13816  rnglz  13948  qusmulrng  14536  quscrng  14537  dvdsrzring  14607  lgsprme0  15761  gausslemma2dlem0e  15772  gausslemma2dlem1a  15777  gausslemma2dlem6  15786  lgsquadlem2  15797  2lgsoddprm  15832  usgrislfuspgrdom  16029  edgssv2en  16038  umgr2edg  16046  uspgredg2v  16060  vtxdfifiun  16103