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  1859  sbidm  1900  disamis  2194  r19.28v  2673  fun11uni  5431  fabexg  5559  fores  5605  f1oabexg  5631  fun11iun  5640  fdmeu  5725  fvelrnb  5729  ssimaex  5743  foeqcnvco  5969  f1eqcocnv  5970  isoini  5997  brtposg  6498  tfrcllemssrecs  6596  fiintim  7204  djuex  7347  elni2  7645  dmaddpqlem  7708  nqpi  7709  ltexnqq  7739  nq0nn  7773  nqnq0a  7785  nqnq0m  7786  elnp1st2nd  7807  mullocprlem  7901  cnegexlem3  8466  divmulasscomap  8987  lediv2a  9186  btwnz  9715  eluz2b2  9953  uz2mulcl  9958  eqreznegel  9964  elioo4g  10286  fz0fzelfz0  10483  fz0fzdiffz0  10486  2ffzeq  10497  elfzodifsumelfzo  10568  elfzom1elp1fzo  10569  zpnn0elfzo  10574  infssuzex  10615  ioo0  10643  zmodidfzoimp  10740  expcl2lemap  10937  hashfibclem  11231  iswrdsymb  11267  ccatcl  11306  ccatsymb  11315  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  pfxswrd  11423  pfxccatin12lem3  11449  pfxccatpfx2  11454  swrdccat3blem  11456  reuccatpfxs1  11464  mulreap  11574  redivap  11584  imdivap  11591  caucvgrelemcau  11690  zproddc  12290  fprodseq  12294  p1modz1  12505  negdvdsb  12518  muldvds1  12527  muldvds2  12528  dvdsdivcl  12561  nn0ehalf  12614  nn0oddm1d2  12620  nnoddm1d2  12621  divgcdnn  12696  coprmgcdb  12810  divgcdcoprm0  12823  pw2dvdslemn  12887  oddprmdvds  13077  4sqexercise1  13121  4sqexercise2  13122  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemth  13225  grpissubg  13947  ecqusaddd  13991  ecqusaddcl  13992  rnglz  14184  qusmulrng  14806  quscrng  14807  dvdsrzring  14877  lgsprme0  16041  gausslemma2dlem0e  16052  gausslemma2dlem1a  16057  gausslemma2dlem6  16066  lgsquadlem2  16077  2lgsoddprm  16112  usgrislfuspgrdom  16311  edgssv2en  16320  umgr2edg  16328  uspgredg2v  16342  subupgr  16394  subusgr  16396  vtxdfifiun  16418  eupth2lem3lem3fi  16591