Theorem anim1i 336

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 334	1 |- ( ( ph /\ ch ) -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl1  397  sylanr1  399  mpan10  463  sbcof2  1762  sbidm  1803  disamis  2084  r19.28v  2532  fun11uni  5149  fabexg  5266  fores  5310  f1oabexg  5333  fun11iun  5342  fvelrnb  5421  ssimaex  5434  foeqcnvco  5643  f1eqcocnv  5644  isoini  5671  brtposg  6103  tfrcllemssrecs  6201  fiintim  6768  djuex  6878  elni2  7064  dmaddpqlem  7127  nqpi  7128  ltexnqq  7158  nq0nn  7192  nqnq0a  7204  nqnq0m  7205  elnp1st2nd  7226  mullocprlem  7320  cnegexlem3  7856  divmulasscomap  8363  lediv2a  8557  btwnz  9068  eluz2b2  9293  uz2mulcl  9298  eqreznegel  9302  elioo4g  9604  fz0fzelfz0  9791  fz0fzdiffz0  9794  2ffzeq  9805  elfzodifsumelfzo  9865  elfzom1elp1fzo  9866  zpnn0elfzo  9871  ioo0  9924  zmodidfzoimp  10014  expcl2lemap  10192  mulreap  10523  redivap  10533  imdivap  10540  caucvgrelemcau  10638  negdvdsb  11351  muldvds1  11360  muldvds2  11361  dvdsdivcl  11390  nn0ehalf  11442  nn0oddm1d2  11448  nnoddm1d2  11449  infssuzex  11484  divgcdnn  11505  coprmgcdb  11609  divgcdcoprm0  11622  pw2dvdslemn  11682