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  9451  harwdom  9499  divalglem6  16358  strleun  17118  oppcbas  17675  sratset  21170  srads  21172  tngvsca  24621  birthdaylem3  26930  birthday  26931  divsqrsum  26959  harmonicbnd  26981  lgslem4  27277  lgscllem  27281  lgsdir2lem2  27303  mulog2sum  27514  vmalogdivsum2  27515  siilem2  30938  h2hva  31060  h2hsm  31061  hhssabloi  31348  elunop2  32099  1fldgenq  33398  zlmds  34122  zlmtset  34123  wallispilem3  46513  wallispilem4  46514  prstcbas  50041  cnelsubclem  50090