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 ⊢ 𝜓

Syntax hints:   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  hartogslem2  9506  harwdom  9554  divalglem6  16457  strleun  17218  oppcbas  17775  sratset  21285  srads  21287  tngvsca  24784  birthdaylem3  27096  birthday  27097  divsqrsum  27124  harmonicbnd  27146  lgslem4  27442  lgscllem  27446  lgsdir2lem2  27468  mulog2sum  27679  vmalogdivsum2  27680  siilem2  31182  h2hva  31304  h2hsm  31305  hhssabloi  31592  elunop2  32343  1fldgenq  33621  zlmds  34330  zlmtset  34331  wallispilem3  46761  wallispilem4  46762  prstcbas  50309  cnelsubclem  50358