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  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5446  fabexg  5574  fores  5620  f1oabexg  5646  fun11iun  5655  fdmeu  5740  fvelrnb  5744  ssimaex  5758  foeqcnvco  5986  f1eqcocnv  5987  isoini  6014  brtposg  6515  tfrcllemssrecs  6613  fiintim  7228  djuex  7373  elni2  7671  dmaddpqlem  7734  nqpi  7735  ltexnqq  7765  nq0nn  7799  nqnq0a  7811  nqnq0m  7812  elnp1st2nd  7833  mullocprlem  7927  cnegexlem3  8493  divmulasscomap  9016  lediv2a  9215  btwnz  9744  eluz2b2  9982  uz2mulcl  9987  eqreznegel  9993  elioo4g  10315  fz0fzelfz0  10512  fz0fzdiffz0  10515  2ffzeq  10526  elfzodifsumelfzo  10597  elfzom1elp1fzo  10598  zpnn0elfzo  10603  infssuzex  10644  ioo0  10672  zmodidfzoimp  10769  expcl2lemap  10966  hashfibclem  11260  iswrdsymb  11300  ccatcl  11339  ccatsymb  11348  swrdfv2  11413  swrdsbslen  11416  swrdspsleq  11417  pfxswrd  11456  pfxccatin12lem3  11482  pfxccatpfx2  11487  swrdccat3blem  11489  reuccatpfxs1  11497  mulreap  11607  redivap  11617  imdivap  11624  caucvgrelemcau  11724  zproddc  12324  fprodseq  12328  p1modz1  12539  negdvdsb  12552  muldvds1  12561  muldvds2  12562  dvdsdivcl  12595  nn0ehalf  12648  nn0oddm1d2  12654  nnoddm1d2  12655  divgcdnn  12730  coprmgcdb  12844  divgcdcoprm0  12857  pw2dvdslemn  12921  oddprmdvds  13111  4sqexercise1  13155  4sqexercise2  13156  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemth  13259  grpissubg  13974  ecqusaddd  14018  ecqusaddcl  14019  rnglz  14219  qusmulrng  14841  quscrng  14842  dvdsrzring  14910  lgsprme0  16075  gausslemma2dlem0e  16086  gausslemma2dlem1a  16091  gausslemma2dlem6  16100  lgsquadlem2  16111  2lgsoddprm  16146  usgrislfuspgrdom  16345  edgssv2en  16354  umgr2edg  16362  uspgredg2v  16376  subupgr  16428  subusgr  16430  vtxdfifiun  16452  eupth2lem3lem3fi  16625