Theorem simp2i 1176

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 1173	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  hartogslem2  8717  harwdom  8764  divalglem6  15495  strleun  16331  birthdaylem3  25093  birthday  25094  divsqrsum  25121  harmonicbnd  25143  lgslem4  25438  lgscllem  25442  lgsdir2lem2  25464  mulog2sum  25639  vmalogdivsum2  25640  siilem2  28262  h2hva  28386  h2hsm  28387  hhssabloi  28674  elunop2  29427  wallispilem3  41078  wallispilem4  41079