Theorem simp2i 1071

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

Syntax hints:   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  hartogslem2  8448  harwdom  8495  divalglem6  15121  strleun  15972  birthdaylem3  24680  birthday  24681  divsqrsum  24708  harmonicbnd  24730  lgslem4  25025  lgscllem  25029  lgsdir2lem2  25051  mulog2sum  25226  vmalogdivsum2  25227  siilem2  27707  h2hva  27831  h2hsm  27832  hhssabloi  28119  elunop2  28872  wallispilem3  40284  wallispilem4  40285