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 207  df-an 396  df-3an 1088

This theorem is referenced by:  hartogslem2  9581  harwdom  9629  divalglem6  16432  strleun  17191  oppcbas  17764  sratset  21206  srads  21209  tngvsca  24680  birthdaylem3  27011  birthday  27012  divsqrsum  27040  harmonicbnd  27062  lgslem4  27359  lgscllem  27363  lgsdir2lem2  27385  mulog2sum  27596  vmalogdivsum2  27597  siilem2  30881  h2hva  31003  h2hsm  31004  hhssabloi  31291  elunop2  32042  1fldgenq  33304  zlmds  33923  zlmtset  33925  wallispilem3  46023  wallispilem4  46024  prstcbas  48868