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  1858  sbidm  1899  disamis  2191  r19.28v  2661  fun11uni  5400  fabexg  5524  fores  5569  f1oabexg  5595  fun11iun  5604  fdmeu  5689  fvelrnb  5693  ssimaex  5707  foeqcnvco  5930  f1eqcocnv  5931  isoini  5958  brtposg  6419  tfrcllemssrecs  6517  fiintim  7122  djuex  7241  elni2  7533  dmaddpqlem  7596  nqpi  7597  ltexnqq  7627  nq0nn  7661  nqnq0a  7673  nqnq0m  7674  elnp1st2nd  7695  mullocprlem  7789  cnegexlem3  8355  divmulasscomap  8875  lediv2a  9074  btwnz  9598  eluz2b2  9836  uz2mulcl  9841  eqreznegel  9847  elioo4g  10168  fz0fzelfz0  10361  fz0fzdiffz0  10364  2ffzeq  10375  elfzodifsumelfzo  10445  elfzom1elp1fzo  10446  zpnn0elfzo  10451  infssuzex  10492  ioo0  10518  zmodidfzoimp  10615  expcl2lemap  10812  iswrdsymb  11130  ccatcl  11169  ccatsymb  11178  swrdfv2  11243  swrdsbslen  11246  swrdspsleq  11247  pfxswrd  11286  pfxccatin12lem3  11312  pfxccatpfx2  11317  swrdccat3blem  11319  reuccatpfxs1  11327  mulreap  11424  redivap  11434  imdivap  11441  caucvgrelemcau  11540  zproddc  12139  fprodseq  12143  p1modz1  12354  negdvdsb  12367  muldvds1  12376  muldvds2  12377  dvdsdivcl  12410  nn0ehalf  12463  nn0oddm1d2  12469  nnoddm1d2  12470  divgcdnn  12545  coprmgcdb  12659  divgcdcoprm0  12672  pw2dvdslemn  12736  oddprmdvds  12926  4sqexercise1  12970  4sqexercise2  12971  grpissubg  13780  ecqusaddd  13824  ecqusaddcl  13825  rnglz  13957  qusmulrng  14545  quscrng  14546  dvdsrzring  14616  lgsprme0  15770  gausslemma2dlem0e  15781  gausslemma2dlem1a  15786  gausslemma2dlem6  15795  lgsquadlem2  15806  2lgsoddprm  15841  usgrislfuspgrdom  16040  edgssv2en  16049  umgr2edg  16057  uspgredg2v  16071  subupgr  16123  subusgr  16125  vtxdfifiun  16147