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  1820  sbidm  1861  disamis  2147  r19.28v  2615  fun11uni  5298  fabexg  5415  fores  5459  f1oabexg  5485  fun11iun  5494  fvelrnb  5576  ssimaex  5590  foeqcnvco  5804  f1eqcocnv  5805  isoini  5832  brtposg  6268  tfrcllemssrecs  6366  fiintim  6941  djuex  7055  elni2  7326  dmaddpqlem  7389  nqpi  7390  ltexnqq  7420  nq0nn  7454  nqnq0a  7466  nqnq0m  7467  elnp1st2nd  7488  mullocprlem  7582  cnegexlem3  8147  divmulasscomap  8666  lediv2a  8865  btwnz  9385  eluz2b2  9616  uz2mulcl  9621  eqreznegel  9627  elioo4g  9947  fz0fzelfz0  10140  fz0fzdiffz0  10143  2ffzeq  10154  elfzodifsumelfzo  10214  elfzom1elp1fzo  10215  zpnn0elfzo  10220  ioo0  10273  zmodidfzoimp  10367  expcl2lemap  10545  mulreap  10886  redivap  10896  imdivap  10903  caucvgrelemcau  11002  zproddc  11600  fprodseq  11604  p1modz1  11814  negdvdsb  11827  muldvds1  11836  muldvds2  11837  dvdsdivcl  11869  nn0ehalf  11921  nn0oddm1d2  11927  nnoddm1d2  11928  infssuzex  11963  divgcdnn  11989  coprmgcdb  12101  divgcdcoprm0  12114  pw2dvdslemn  12178  oddprmdvds  12365  grpissubg  13085  rnglz  13195  dvdsrzring  13750  lgsprme0  14714