Theorem simp2i 1146

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

Syntax hints:   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  hartogslem2  9455  harwdom  9503  divalglem6  16365  strleun  17125  oppcbas  17682  sratset  21180  srads  21182  tngvsca  24636  birthdaylem3  26942  birthday  26943  divsqrsum  26970  harmonicbnd  26992  lgslem4  27288  lgscllem  27292  lgsdir2lem2  27314  mulog2sum  27525  vmalogdivsum2  27526  siilem2  30948  h2hva  31070  h2hsm  31071  hhssabloi  31358  elunop2  32109  1fldgenq  33413  zlmds  34153  zlmtset  34154  wallispilem3  46517  wallispilem4  46518  prstcbas  50051  cnelsubclem  50100