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  9010  harwdom  9057  divalglem6  15752  strleun  16594  birthdaylem3  25534  birthday  25535  divsqrsum  25562  harmonicbnd  25584  lgslem4  25879  lgscllem  25883  lgsdir2lem2  25905  mulog2sum  26116  vmalogdivsum2  26117  siilem2  28632  h2hva  28754  h2hsm  28755  hhssabloi  29042  elunop2  29793  wallispilem3  42359  wallispilem4  42360