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

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  hartogslem2  9564  harwdom  9612  divalglem6  16597  strleun  17364  oppcbas  17921  sratset  21488  srads  21490  tngvsca  24995  birthdaylem3  27311  birthday  27312  divsqrsum  27339  harmonicbnd  27361  lgslem4  27657  lgscllem  27661  lgsdir2lem2  27683  mulog2sum  27894  vmalogdivsum2  27895  siilem2  31484  h2hva  31606  h2hsm  31607  hhssabloi  31894  elunop2  32645  1fldgenq  33954  zlmds  34664  zlmtset  34665  wallispilem3  47282  wallispilem4  47283  prstcbas  50897  cnelsubcw  50946  parswapfunc  50983  par2diag  50985  fuconuniqlem  50986  fuconuniqvalslem  50988