Theorem simp2i 1140

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

Syntax hints:   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  hartogslem2  9429  harwdom  9477  divalglem6  16306  strleun  17065  oppcbas  17621  sratset  21115  srads  21117  tngvsca  24559  birthdaylem3  26888  birthday  26889  divsqrsum  26917  harmonicbnd  26939  lgslem4  27236  lgscllem  27240  lgsdir2lem2  27262  mulog2sum  27473  vmalogdivsum2  27474  siilem2  30827  h2hva  30949  h2hsm  30950  hhssabloi  31237  elunop2  31988  1fldgenq  33283  zlmds  33970  zlmtset  33971  wallispilem3  46104  wallispilem4  46105  prstcbas  49585  cnelsubclem  49634