Theorem simp2i 1147

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

Syntax hints:   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  hartogslem2  9452  harwdom  9500  divalglem6  16362  strleun  17122  oppcbas  17679  sratset  21176  srads  21178  tngvsca  24632  birthdaylem3  26938  birthday  26939  divsqrsum  26966  harmonicbnd  26988  lgslem4  27284  lgscllem  27288  lgsdir2lem2  27310  mulog2sum  27521  vmalogdivsum2  27522  siilem2  30943  h2hva  31065  h2hsm  31066  hhssabloi  31353  elunop2  32104  1fldgenq  33408  zlmds  34156  zlmtset  34157  wallispilem3  46522  wallispilem4  46523  prstcbas  50056  cnelsubclem  50105