Theorem simp2i 1006

Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis

Ref	Expression
3simp1i.1	|- ( ph /\ ps /\ ch )

Assertion

Ref	Expression
simp2i	|- ps

Proof of Theorem simp2i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 |- ( ph /\ ps /\ ch )
2		simp2 997	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

Syntax hints:   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975

This theorem is referenced by:  hartogslem2  7986  harwdom  8034  divalglem6  14068  strleun  14742  birthdaylem3  23409  birthday  23410  divsqrsum  23437  harmonicbnd  23459  lgslem4  23700  lgscllem  23704  lgsdir2lem2  23725  mulog2sum  23848  vmalogdivsum2  23849  siilem2  25894  h2hva  26018  h2hsm  26019  hhssabloi  26305  elunop2  27059  wallispilem3  32052  wallispilem4  32053