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  9519  harwdom  9567  divalglem6  16494  strleun  17255  oppcbas  17812  sratset  21373  srads  21375  tngvsca  24878  birthdaylem3  27198  birthday  27199  divsqrsum  27226  harmonicbnd  27248  lgslem4  27544  lgscllem  27548  lgsdir2lem2  27570  mulog2sum  27781  vmalogdivsum2  27782  siilem2  31341  h2hva  31463  h2hsm  31464  hhssabloi  31751  elunop2  32502  1fldgenq  33771  zlmds  34480  zlmtset  34481  wallispilem3  46903  wallispilem4  46904  prstcbas  50488  cnelsubclem  50537