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  1821  sbidm  1862  disamis  2153  r19.28v  2622  fun11uni  5325  fabexg  5442  fores  5487  f1oabexg  5513  fun11iun  5522  fvelrnb  5605  ssimaex  5619  foeqcnvco  5834  f1eqcocnv  5835  isoini  5862  brtposg  6309  tfrcllemssrecs  6407  fiintim  6987  djuex  7104  elni2  7376  dmaddpqlem  7439  nqpi  7440  ltexnqq  7470  nq0nn  7504  nqnq0a  7516  nqnq0m  7517  elnp1st2nd  7538  mullocprlem  7632  cnegexlem3  8198  divmulasscomap  8717  lediv2a  8916  btwnz  9439  eluz2b2  9671  uz2mulcl  9676  eqreznegel  9682  elioo4g  10003  fz0fzelfz0  10196  fz0fzdiffz0  10199  2ffzeq  10210  elfzodifsumelfzo  10271  elfzom1elp1fzo  10272  zpnn0elfzo  10277  ioo0  10331  zmodidfzoimp  10428  expcl2lemap  10625  iswrdsymb  10935  mulreap  11011  redivap  11021  imdivap  11028  caucvgrelemcau  11127  zproddc  11725  fprodseq  11729  p1modz1  11940  negdvdsb  11953  muldvds1  11962  muldvds2  11963  dvdsdivcl  11995  nn0ehalf  12047  nn0oddm1d2  12053  nnoddm1d2  12054  infssuzex  12089  divgcdnn  12115  coprmgcdb  12229  divgcdcoprm0  12242  pw2dvdslemn  12306  oddprmdvds  12495  4sqexercise1  12539  4sqexercise2  12540  grpissubg  13267  ecqusaddd  13311  ecqusaddcl  13312  rnglz  13444  qusmulrng  14031  quscrng  14032  dvdsrzring  14102  lgsprme0  15199  gausslemma2dlem0e  15210  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  lgsquadlem2  15235  2lgsoddprm  15270