Theorem anim1i 338

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylanl1  400  sylanr1  402  mpan10  466  sbcof2  1787  sbidm  1828  disamis  2114  r19.28v  2582  fun11uni  5233  fabexg  5350  fores  5394  f1oabexg  5419  fun11iun  5428  fvelrnb  5509  ssimaex  5522  foeqcnvco  5731  f1eqcocnv  5732  isoini  5759  brtposg  6191  tfrcllemssrecs  6289  fiintim  6862  djuex  6973  elni2  7213  dmaddpqlem  7276  nqpi  7277  ltexnqq  7307  nq0nn  7341  nqnq0a  7353  nqnq0m  7354  elnp1st2nd  7375  mullocprlem  7469  cnegexlem3  8031  divmulasscomap  8548  lediv2a  8745  btwnz  9262  eluz2b2  9492  uz2mulcl  9497  eqreznegel  9501  elioo4g  9816  fz0fzelfz0  10004  fz0fzdiffz0  10007  2ffzeq  10018  elfzodifsumelfzo  10078  elfzom1elp1fzo  10079  zpnn0elfzo  10084  ioo0  10137  zmodidfzoimp  10231  expcl2lemap  10409  mulreap  10741  redivap  10751  imdivap  10758  caucvgrelemcau  10857  zproddc  11453  fprodseq  11457  negdvdsb  11676  muldvds1  11685  muldvds2  11686  dvdsdivcl  11715  nn0ehalf  11767  nn0oddm1d2  11773  nnoddm1d2  11774  infssuzex  11809  divgcdnn  11831  coprmgcdb  11937  divgcdcoprm0  11950  pw2dvdslemn  12011