Theorem simp2i 1019

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

Syntax hints:   /\ w3a 986

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 189  df-an 373  df-3an 988

This theorem is referenced by:  hartogslem2  8063  harwdom  8110  divalglem6  14390  strleun  15232  birthdaylem3  23891  birthday  23892  divsqrsum  23919  harmonicbnd  23941  lgslem4  24239  lgscllem  24243  lgsdir2lem2  24264  mulog2sum  24387  vmalogdivsum2  24388  siilem2  26505  h2hva  26639  h2hsm  26640  hhssabloi  26925  elunop2  27678  wallispilem3  37939  wallispilem4  37940