Theorem simp2i 1156

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

Syntax hints:   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  hartogslem2  9493  harwdom  9541  divalglem6  16446  strleun  17207  oppcbas  17764  sratset  21273  srads  21275  tngvsca  24764  birthdaylem3  27076  birthday  27077  divsqrsum  27104  harmonicbnd  27126  lgslem4  27422  lgscllem  27426  lgsdir2lem2  27448  mulog2sum  27659  vmalogdivsum2  27660  siilem2  31113  h2hva  31235  h2hsm  31236  hhssabloi  31523  elunop2  32274  1fldgenq  33558  zlmds  34269  zlmtset  34270  wallispilem3  46639  wallispilem4  46640  prstcbas  50183  cnelsubclem  50232