Theorem simp2i 1152

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

Syntax hints:   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  hartogslem2  9488  harwdom  9536  divalglem6  16415  strleun  17176  oppcbas  17733  sratset  21230  srads  21232  tngvsca  24686  birthdaylem3  26995  birthday  26996  divsqrsum  27023  harmonicbnd  27045  lgslem4  27341  lgscllem  27345  lgsdir2lem2  27367  mulog2sum  27578  vmalogdivsum2  27579  siilem2  31001  h2hva  31123  h2hsm  31124  hhssabloi  31411  elunop2  32162  1fldgenq  33470  zlmds  34220  zlmtset  34221  wallispilem3  46605  wallispilem4  46606  prstcbas  50139  cnelsubclem  50188