Theorem simp2i 1158

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

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  hartogslem2  9515  harwdom  9563  divalglem6  16481  strleun  17242  oppcbas  17799  sratset  21341  srads  21343  tngvsca  24840  birthdaylem3  27155  birthday  27156  divsqrsum  27183  harmonicbnd  27205  lgslem4  27501  lgscllem  27505  lgsdir2lem2  27527  mulog2sum  27738  vmalogdivsum2  27739  siilem2  31241  h2hva  31363  h2hsm  31364  hhssabloi  31651  elunop2  32402  1fldgenq  33674  zlmds  34383  zlmtset  34384  wallispilem3  46822  wallispilem4  46823  prstcbas  50373  cnelsubclem  50422  rr3fv2cli  50671