Theorem simp2i 1141

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 1138	. 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  hartogslem2  9460  harwdom  9508  divalglem6  16337  strleun  17096  oppcbas  17653  sratset  21147  srads  21149  tngvsca  24602  birthdaylem3  26931  birthday  26932  divsqrsum  26960  harmonicbnd  26982  lgslem4  27279  lgscllem  27283  lgsdir2lem2  27305  mulog2sum  27516  vmalogdivsum2  27517  siilem2  30939  h2hva  31061  h2hsm  31062  hhssabloi  31349  elunop2  32100  1fldgenq  33415  zlmds  34139  zlmtset  34140  wallispilem3  46419  wallispilem4  46420  prstcbas  49907  cnelsubclem  49956