Theorem simp2i 1001

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 992	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
3	1, 2	ax-mp 5	1 |- ps

Syntax hints:   /\ w3a 968

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 970

This theorem is referenced by:  hartogslem2  7957  harwdom  8005  divalglem6  13904  strleun  14574  birthdaylem3  23004  birthday  23005  divsqrsum  23032  harmonicbnd  23054  lgslem4  23295  lgscllem  23299  lgsdir2lem2  23320  mulog2sum  23443  vmalogdivsum2  23444  siilem2  25293  h2hva  25417  h2hsm  25418  hhssabloi  25704  elunop2  26458  wallispilem3  31186  wallispilem4  31187