Theorem simp2i 1137

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

Hypothesis

Ref	Expression
3simp1i.1	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Assertion

Ref	Expression
simp2i	⊢ 𝜓

Proof of Theorem simp2i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
2		simp2 1134	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  hartogslem2  8991  harwdom  9039  divalglem6  15739  strleun  16583  birthdaylem3  25539  birthday  25540  divsqrsum  25567  harmonicbnd  25589  lgslem4  25884  lgscllem  25888  lgsdir2lem2  25910  mulog2sum  26121  vmalogdivsum2  26122  siilem2  28635  h2hva  28757  h2hsm  28758  hhssabloi  29045  elunop2  29796  wallispilem3  42709  wallispilem4  42710