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 1087

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 1089

This theorem is referenced by:  hartogslem2  9612  harwdom  9660  divalglem6  16446  strleun  17204  oppcbas  17777  sratset  21211  srads  21214  tngvsca  24685  birthdaylem3  27014  birthday  27015  divsqrsum  27043  harmonicbnd  27065  lgslem4  27362  lgscllem  27366  lgsdir2lem2  27388  mulog2sum  27599  vmalogdivsum2  27600  siilem2  30884  h2hva  31006  h2hsm  31007  hhssabloi  31294  elunop2  32045  1fldgenq  33289  zlmds  33908  zlmtset  33910  wallispilem3  45988  wallispilem4  45989  prstcbas  48734