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  9448  harwdom  9496  divalglem6  16325  strleun  17084  oppcbas  17641  sratset  21135  srads  21137  tngvsca  24590  birthdaylem3  26919  birthday  26920  divsqrsum  26948  harmonicbnd  26970  lgslem4  27267  lgscllem  27271  lgsdir2lem2  27293  mulog2sum  27504  vmalogdivsum2  27505  siilem2  30927  h2hva  31049  h2hsm  31050  hhssabloi  31337  elunop2  32088  1fldgenq  33404  zlmds  34119  zlmtset  34120  wallispilem3  46307  wallispilem4  46308  prstcbas  49795  cnelsubclem  49844