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  1832  sbidm  1873  disamis  2164  r19.28v  2633  fun11uni  5343  fabexg  5462  fores  5507  f1oabexg  5533  fun11iun  5542  fvelrnb  5625  ssimaex  5639  foeqcnvco  5858  f1eqcocnv  5859  isoini  5886  brtposg  6339  tfrcllemssrecs  6437  fiintim  7027  djuex  7144  elni2  7426  dmaddpqlem  7489  nqpi  7490  ltexnqq  7520  nq0nn  7554  nqnq0a  7566  nqnq0m  7567  elnp1st2nd  7588  mullocprlem  7682  cnegexlem3  8248  divmulasscomap  8768  lediv2a  8967  btwnz  9491  eluz2b2  9723  uz2mulcl  9728  eqreznegel  9734  elioo4g  10055  fz0fzelfz0  10248  fz0fzdiffz0  10251  2ffzeq  10262  elfzodifsumelfzo  10328  elfzom1elp1fzo  10329  zpnn0elfzo  10334  infssuzex  10374  ioo0  10400  zmodidfzoimp  10497  expcl2lemap  10694  iswrdsymb  11010  ccatcl  11047  ccatsymb  11056  mulreap  11146  redivap  11156  imdivap  11163  caucvgrelemcau  11262  zproddc  11861  fprodseq  11865  p1modz1  12076  negdvdsb  12089  muldvds1  12098  muldvds2  12099  dvdsdivcl  12132  nn0ehalf  12185  nn0oddm1d2  12191  nnoddm1d2  12192  divgcdnn  12267  coprmgcdb  12381  divgcdcoprm0  12394  pw2dvdslemn  12458  oddprmdvds  12648  4sqexercise1  12692  4sqexercise2  12693  grpissubg  13501  ecqusaddd  13545  ecqusaddcl  13546  rnglz  13678  qusmulrng  14265  quscrng  14266  dvdsrzring  14336  lgsprme0  15490  gausslemma2dlem0e  15501  gausslemma2dlem1a  15506  gausslemma2dlem6  15515  lgsquadlem2  15526  2lgsoddprm  15561