Theorem simp2i 1139

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 1136	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  hartogslem2  9290  harwdom  9338  divalglem6  16118  strleun  16869  oppcbas  17439  sratset  20463  srads  20466  tngvsca  23818  birthdaylem3  26114  birthday  26115  divsqrsum  26142  harmonicbnd  26164  lgslem4  26459  lgscllem  26463  lgsdir2lem2  26485  mulog2sum  26696  vmalogdivsum2  26697  siilem2  29223  h2hva  29345  h2hsm  29346  hhssabloi  29633  elunop2  30384  zlmds  31921  zlmtset  31923  wallispilem3  43590  wallispilem4  43591  prstcbas  46327