Theorem simp2i 1140

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

Syntax hints:   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  hartogslem2  9350  harwdom  9398  divalglem6  16156  strleun  16907  oppcbas  17477  sratset  20501  srads  20504  tngvsca  23856  birthdaylem3  26152  birthday  26153  divsqrsum  26180  harmonicbnd  26202  lgslem4  26497  lgscllem  26501  lgsdir2lem2  26523  mulog2sum  26734  vmalogdivsum2  26735  siilem2  29263  h2hva  29385  h2hsm  29386  hhssabloi  29673  elunop2  30424  zlmds  31961  zlmtset  31963  wallispilem3  43837  wallispilem4  43838  prstcbas  46592