Theorem simp2i 1138

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

Syntax hints:   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  hartogslem2  9263  harwdom  9311  divalglem6  16088  strleun  16839  oppcbas  17409  sratset  20433  srads  20436  tngvsca  23788  birthdaylem3  26084  birthday  26085  divsqrsum  26112  harmonicbnd  26134  lgslem4  26429  lgscllem  26433  lgsdir2lem2  26455  mulog2sum  26666  vmalogdivsum2  26667  siilem2  29193  h2hva  29315  h2hsm  29316  hhssabloi  29603  elunop2  30354  zlmds  31891  zlmtset  31893  wallispilem3  43562  wallispilem4  43563  prstcbas  46300