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  9503  harwdom  9551  divalglem6  16375  strleun  17134  oppcbas  17686  sratset  21097  srads  21099  tngvsca  24541  birthdaylem3  26870  birthday  26871  divsqrsum  26899  harmonicbnd  26921  lgslem4  27218  lgscllem  27222  lgsdir2lem2  27244  mulog2sum  27455  vmalogdivsum2  27456  siilem2  30788  h2hva  30910  h2hsm  30911  hhssabloi  31198  elunop2  31949  1fldgenq  33279  zlmds  33959  zlmtset  33960  wallispilem3  46072  wallispilem4  46073  prstcbas  49547  cnelsubclem  49596