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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanl1  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5454  fabexg  5582  fores  5628  f1oabexg  5654  fun11iun  5663  fdmeu  5749  fvelrnb  5753  ssimaex  5767  foeqcnvco  5999  f1eqcocnv  6000  isoini  6027  brtposg  6529  tfrcllemssrecs  6627  fiintim  7242  djuex  7389  elni2  7687  dmaddpqlem  7750  nqpi  7751  ltexnqq  7781  nq0nn  7815  nqnq0a  7827  nqnq0m  7828  elnp1st2nd  7849  mullocprlem  7943  cnegexlem3  8510  divmulasscomap  9034  lediv2a  9233  btwnz  9776  eluz2b2  10019  uz2mulcl  10024  eqreznegel  10030  elioo4g  10353  fz0fzelfz0  10551  fz0fzdiffz0  10554  2ffzeq  10565  elfzodifsumelfzo  10636  elfzom1elp1fzo  10637  zpnn0elfzo  10642  infssuzex  10683  ioo0  10711  zmodidfzoimp  10812  expcl2lemap  11009  hashfibclem  11304  iswrdsymb  11344  ccatcl  11383  ccatsymb  11392  swrdfv2  11457  swrdsbslen  11460  swrdspsleq  11461  pfxswrd  11500  pfxccatin12lem3  11526  pfxccatpfx2  11531  swrdccat3blem  11533  reuccatpfxs1  11541  mulreap  11651  redivap  11661  imdivap  11668  caucvgrelemcau  11768  zproddc  12371  fprodseq  12375  p1modz1  12586  negdvdsb  12599  muldvds1  12608  muldvds2  12609  dvdsdivcl  12642  nn0ehalf  12695  nn0oddm1d2  12701  nnoddm1d2  12702  divgcdnn  12777  coprmgcdb  12891  divgcdcoprm0  12904  pwbdvdslemn  12969  oddprmdvds  13162  4sqexercise1  13206  4sqexercise2  13207  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemth  13339  grpissubg  14056  ecqusaddd  14100  ecqusaddcl  14101  rnglz  14351  qusmulrng  14978  quscrng  14979  dvdsrzring  15047  bcmono  16304  lgsprme0  16366  gausslemma2dlem0e  16377  gausslemma2dlem1a  16382  gausslemma2dlem6  16391  lgsquadlem2  16402  2lgsoddprm  16437  usgrislfuspgrdom  16636  edgssv2en  16645  umgr2edg  16653  uspgredg2v  16667  subupgr  16719  subusgr  16721  vtxdfifiun  16743  eupth2lem3lem3fi  16916