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 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  9436  harwdom  9484  divalglem6  16311  strleun  17070  oppcbas  17626  sratset  21119  srads  21121  tngvsca  24562  birthdaylem3  26891  birthday  26892  divsqrsum  26920  harmonicbnd  26942  lgslem4  27239  lgscllem  27243  lgsdir2lem2  27265  mulog2sum  27476  vmalogdivsum2  27477  siilem2  30834  h2hva  30956  h2hsm  30957  hhssabloi  31244  elunop2  31995  1fldgenq  33295  zlmds  33996  zlmtset  33997  wallispilem3  46189  wallispilem4  46190  prstcbas  49679  cnelsubclem  49728