Theorem simp2i 1136

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

Syntax hints:   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  hartogslem2  9007  harwdom  9054  divalglem6  15749  strleun  16591  birthdaylem3  25531  birthday  25532  divsqrsum  25559  harmonicbnd  25581  lgslem4  25876  lgscllem  25880  lgsdir2lem2  25902  mulog2sum  26113  vmalogdivsum2  26114  siilem2  28629  h2hva  28751  h2hsm  28752  hhssabloi  29039  elunop2  29790  wallispilem3  42372  wallispilem4  42373