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  1859  sbidm  1900  disamis  2192  r19.28v  2671  fun11uni  5426  fabexg  5554  fores  5600  f1oabexg  5626  fun11iun  5635  fdmeu  5720  fvelrnb  5724  ssimaex  5738  foeqcnvco  5963  f1eqcocnv  5964  isoini  5991  brtposg  6485  tfrcllemssrecs  6583  fiintim  7191  djuex  7334  elni2  7629  dmaddpqlem  7692  nqpi  7693  ltexnqq  7723  nq0nn  7757  nqnq0a  7769  nqnq0m  7770  elnp1st2nd  7791  mullocprlem  7885  cnegexlem3  8450  divmulasscomap  8970  lediv2a  9169  btwnz  9697  eluz2b2  9935  uz2mulcl  9940  eqreznegel  9946  elioo4g  10267  fz0fzelfz0  10461  fz0fzdiffz0  10464  2ffzeq  10475  elfzodifsumelfzo  10546  elfzom1elp1fzo  10547  zpnn0elfzo  10552  infssuzex  10593  ioo0  10619  zmodidfzoimp  10716  expcl2lemap  10913  hashfibclem  11206  iswrdsymb  11242  ccatcl  11281  ccatsymb  11290  swrdfv2  11355  swrdsbslen  11358  swrdspsleq  11359  pfxswrd  11398  pfxccatin12lem3  11424  pfxccatpfx2  11429  swrdccat3blem  11431  reuccatpfxs1  11439  mulreap  11549  redivap  11559  imdivap  11566  caucvgrelemcau  11665  zproddc  12265  fprodseq  12269  p1modz1  12480  negdvdsb  12493  muldvds1  12502  muldvds2  12503  dvdsdivcl  12536  nn0ehalf  12589  nn0oddm1d2  12595  nnoddm1d2  12596  divgcdnn  12671  coprmgcdb  12785  divgcdcoprm0  12798  pw2dvdslemn  12862  oddprmdvds  13052  4sqexercise1  13096  4sqexercise2  13097  grpissubg  13911  ecqusaddd  13955  ecqusaddcl  13956  rnglz  14089  qusmulrng  14680  quscrng  14681  dvdsrzring  14751  lgsprme0  15915  gausslemma2dlem0e  15926  gausslemma2dlem1a  15931  gausslemma2dlem6  15940  lgsquadlem2  15951  2lgsoddprm  15986  usgrislfuspgrdom  16185  edgssv2en  16194  umgr2edg  16202  uspgredg2v  16216  subupgr  16268  subusgr  16270  vtxdfifiun  16292  eupth2lem3lem3fi  16465