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  6530  tfrcllemssrecs  6628  fiintim  7244  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  9775  eluz2b2  10018  uz2mulcl  10023  eqreznegel  10029  elioo4g  10352  fz0fzelfz0  10550  fz0fzdiffz0  10553  2ffzeq  10564  elfzodifsumelfzo  10635  elfzom1elp1fzo  10636  zpnn0elfzo  10641  infssuzex  10682  ioo0  10710  zmodidfzoimp  10811  expcl2lemap  11008  hashfibclem  11303  iswrdsymb  11343  ccatcl  11382  ccatsymb  11391  swrdfv2  11456  swrdsbslen  11459  swrdspsleq  11460  pfxswrd  11499  pfxccatin12lem3  11525  pfxccatpfx2  11530  swrdccat3blem  11532  reuccatpfxs1  11540  mulreap  11650  redivap  11660  imdivap  11667  caucvgrelemcau  11767  zproddc  12370  fprodseq  12374  p1modz1  12585  negdvdsb  12598  muldvds1  12607  muldvds2  12608  dvdsdivcl  12641  nn0ehalf  12694  nn0oddm1d2  12700  nnoddm1d2  12701  divgcdnn  12776  coprmgcdb  12890  divgcdcoprm0  12903  pwbdvdslemn  12968  oddprmdvds  13161  4sqexercise1  13205  4sqexercise2  13206  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemth  13338  grpissubg  14055  ecqusaddd  14099  ecqusaddcl  14100  rnglz  14350  qusmulrng  14977  quscrng  14978  dvdsrzring  15046  bcmono  16321  lgsprme0  16383  gausslemma2dlem0e  16394  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  lgsquadlem2  16419  2lgsoddprm  16454  usgrislfuspgrdom  16653  edgssv2en  16662  umgr2edg  16670  uspgredg2v  16684  subupgr  16736  subusgr  16738  vtxdfifiun  16760  eupth2lem3lem3fi  16933