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  471  sbcof2  1803  sbidm  1844  disamis  2130  r19.28v  2598  fun11uni  5268  fabexg  5385  fores  5429  f1oabexg  5454  fun11iun  5463  fvelrnb  5544  ssimaex  5557  foeqcnvco  5769  f1eqcocnv  5770  isoini  5797  brtposg  6233  tfrcllemssrecs  6331  fiintim  6906  djuex  7020  elni2  7276  dmaddpqlem  7339  nqpi  7340  ltexnqq  7370  nq0nn  7404  nqnq0a  7416  nqnq0m  7417  elnp1st2nd  7438  mullocprlem  7532  cnegexlem3  8096  divmulasscomap  8613  lediv2a  8811  btwnz  9331  eluz2b2  9562  uz2mulcl  9567  eqreznegel  9573  elioo4g  9891  fz0fzelfz0  10083  fz0fzdiffz0  10086  2ffzeq  10097  elfzodifsumelfzo  10157  elfzom1elp1fzo  10158  zpnn0elfzo  10163  ioo0  10216  zmodidfzoimp  10310  expcl2lemap  10488  mulreap  10828  redivap  10838  imdivap  10845  caucvgrelemcau  10944  zproddc  11542  fprodseq  11546  p1modz1  11756  negdvdsb  11769  muldvds1  11778  muldvds2  11779  dvdsdivcl  11810  nn0ehalf  11862  nn0oddm1d2  11868  nnoddm1d2  11869  infssuzex  11904  divgcdnn  11930  coprmgcdb  12042  divgcdcoprm0  12055  pw2dvdslemn  12119  oddprmdvds  12306  lgsprme0  13737