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  1810  sbidm  1851  disamis  2137  r19.28v  2605  fun11uni  5288  fabexg  5405  fores  5449  f1oabexg  5475  fun11iun  5484  fvelrnb  5565  ssimaex  5579  foeqcnvco  5793  f1eqcocnv  5794  isoini  5821  brtposg  6257  tfrcllemssrecs  6355  fiintim  6930  djuex  7044  elni2  7315  dmaddpqlem  7378  nqpi  7379  ltexnqq  7409  nq0nn  7443  nqnq0a  7455  nqnq0m  7456  elnp1st2nd  7477  mullocprlem  7571  cnegexlem3  8136  divmulasscomap  8655  lediv2a  8854  btwnz  9374  eluz2b2  9605  uz2mulcl  9610  eqreznegel  9616  elioo4g  9936  fz0fzelfz0  10129  fz0fzdiffz0  10132  2ffzeq  10143  elfzodifsumelfzo  10203  elfzom1elp1fzo  10204  zpnn0elfzo  10209  ioo0  10262  zmodidfzoimp  10356  expcl2lemap  10534  mulreap  10875  redivap  10885  imdivap  10892  caucvgrelemcau  10991  zproddc  11589  fprodseq  11593  p1modz1  11803  negdvdsb  11816  muldvds1  11825  muldvds2  11826  dvdsdivcl  11858  nn0ehalf  11910  nn0oddm1d2  11916  nnoddm1d2  11917  infssuzex  11952  divgcdnn  11978  coprmgcdb  12090  divgcdcoprm0  12103  pw2dvdslemn  12167  oddprmdvds  12354  grpissubg  13059  dvdsrzring  13578  lgsprme0  14528