Theorem simp2i 1158

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

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  hartogslem2  9521  harwdom  9569  divalglem6  16548  strleun  17315  oppcbas  17872  sratset  21438  srads  21440  tngvsca  24945  birthdaylem3  27263  birthday  27264  divsqrsum  27291  harmonicbnd  27313  lgslem4  27609  lgscllem  27613  lgsdir2lem2  27635  mulog2sum  27846  vmalogdivsum2  27847  siilem2  31436  h2hva  31558  h2hsm  31559  hhssabloi  31846  elunop2  32597  1fldgenq  33866  zlmds  34576  zlmtset  34577  wallispilem3  47021  wallispilem4  47022  prstcbas  50606  cnelsubclem  50655