Theorem simp2i 998

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

Syntax hints:   /\ w3a 965

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 967

This theorem is referenced by:  hartogslem2  7858  harwdom  7906  divalglem6  13704  strleun  14370  birthdaylem3  22463  birthday  22464  divsqrsum  22491  harmonicbnd  22513  lgslem4  22754  lgscllem  22758  lgsdir2lem2  22779  mulog2sum  22902  vmalogdivsum2  22903  siilem2  24387  h2hva  24511  h2hsm  24512  hhssabloi  24798  elunop2  25552  wallispilem3  30000  wallispilem4  30001