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  5451  fabexg  5579  fores  5625  f1oabexg  5651  fun11iun  5660  fdmeu  5746  fvelrnb  5750  ssimaex  5764  foeqcnvco  5996  f1eqcocnv  5997  isoini  6024  brtposg  6525  tfrcllemssrecs  6623  fiintim  7238  djuex  7383  elni2  7681  dmaddpqlem  7744  nqpi  7745  ltexnqq  7775  nq0nn  7809  nqnq0a  7821  nqnq0m  7822  elnp1st2nd  7843  mullocprlem  7937  cnegexlem3  8503  divmulasscomap  9026  lediv2a  9225  btwnz  9765  eluz2b2  10003  uz2mulcl  10008  eqreznegel  10014  elioo4g  10336  fz0fzelfz0  10534  fz0fzdiffz0  10537  2ffzeq  10548  elfzodifsumelfzo  10619  elfzom1elp1fzo  10620  zpnn0elfzo  10625  infssuzex  10666  ioo0  10694  zmodidfzoimp  10791  expcl2lemap  10988  hashfibclem  11282  iswrdsymb  11322  ccatcl  11361  ccatsymb  11370  swrdfv2  11435  swrdsbslen  11438  swrdspsleq  11439  pfxswrd  11478  pfxccatin12lem3  11504  pfxccatpfx2  11509  swrdccat3blem  11511  reuccatpfxs1  11519  mulreap  11629  redivap  11639  imdivap  11646  caucvgrelemcau  11746  zproddc  12346  fprodseq  12350  p1modz1  12561  negdvdsb  12574  muldvds1  12583  muldvds2  12584  dvdsdivcl  12617  nn0ehalf  12670  nn0oddm1d2  12676  nnoddm1d2  12677  divgcdnn  12752  coprmgcdb  12866  divgcdcoprm0  12879  pw2dvdslemn  12943  oddprmdvds  13133  4sqexercise1  13177  4sqexercise2  13178  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemth  13281  grpissubg  13997  ecqusaddd  14041  ecqusaddcl  14042  rnglz  14244  qusmulrng  14869  quscrng  14870  dvdsrzring  14938  lgsprme0  16161  gausslemma2dlem0e  16172  gausslemma2dlem1a  16177  gausslemma2dlem6  16186  lgsquadlem2  16197  2lgsoddprm  16232  usgrislfuspgrdom  16431  edgssv2en  16440  umgr2edg  16448  uspgredg2v  16462  subupgr  16514  subusgr  16516  vtxdfifiun  16538  eupth2lem3lem3fi  16711