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  9540  harwdom  9588  divalglem6  16573  strleun  17340  oppcbas  17897  sratset  21463  srads  21465  tngvsca  24970  birthdaylem3  27286  birthday  27287  divsqrsum  27314  harmonicbnd  27336  lgslem4  27632  lgscllem  27636  lgsdir2lem2  27658  mulog2sum  27869  vmalogdivsum2  27870  siilem2  31459  h2hva  31581  h2hsm  31582  hhssabloi  31869  elunop2  32620  1fldgenq  33930  zlmds  34640  zlmtset  34641  wallispilem3  47170  wallispilem4  47171  prstcbas  50785  cnelsubcw  50834  parswapfunc  50871  par2diag  50873  fuconuniqlem  50874  fuconuniqvalslem  50876