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  1858  sbidm  1899  disamis  2191  r19.28v  2662  fun11uni  5407  fabexg  5532  fores  5578  f1oabexg  5604  fun11iun  5613  fdmeu  5698  fvelrnb  5702  ssimaex  5716  foeqcnvco  5941  f1eqcocnv  5942  isoini  5969  brtposg  6463  tfrcllemssrecs  6561  fiintim  7166  djuex  7285  elni2  7577  dmaddpqlem  7640  nqpi  7641  ltexnqq  7671  nq0nn  7705  nqnq0a  7717  nqnq0m  7718  elnp1st2nd  7739  mullocprlem  7833  cnegexlem3  8398  divmulasscomap  8918  lediv2a  9117  btwnz  9643  eluz2b2  9881  uz2mulcl  9886  eqreznegel  9892  elioo4g  10213  fz0fzelfz0  10407  fz0fzdiffz0  10410  2ffzeq  10421  elfzodifsumelfzo  10492  elfzom1elp1fzo  10493  zpnn0elfzo  10498  infssuzex  10539  ioo0  10565  zmodidfzoimp  10662  expcl2lemap  10859  iswrdsymb  11180  ccatcl  11219  ccatsymb  11228  swrdfv2  11293  swrdsbslen  11296  swrdspsleq  11297  pfxswrd  11336  pfxccatin12lem3  11362  pfxccatpfx2  11367  swrdccat3blem  11369  reuccatpfxs1  11377  mulreap  11487  redivap  11497  imdivap  11504  caucvgrelemcau  11603  zproddc  12203  fprodseq  12207  p1modz1  12418  negdvdsb  12431  muldvds1  12440  muldvds2  12441  dvdsdivcl  12474  nn0ehalf  12527  nn0oddm1d2  12533  nnoddm1d2  12534  divgcdnn  12609  coprmgcdb  12723  divgcdcoprm0  12736  pw2dvdslemn  12800  oddprmdvds  12990  4sqexercise1  13034  4sqexercise2  13035  grpissubg  13844  ecqusaddd  13888  ecqusaddcl  13889  rnglz  14022  qusmulrng  14611  quscrng  14612  dvdsrzring  14682  lgsprme0  15844  gausslemma2dlem0e  15855  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  lgsquadlem2  15880  2lgsoddprm  15915  usgrislfuspgrdom  16114  edgssv2en  16123  umgr2edg  16131  uspgredg2v  16145  subupgr  16197  subusgr  16199  vtxdfifiun  16221  eupth2lem3lem3fi  16394