Theorem simp3i 1159

Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis

Ref	Expression
3simp1i.1	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Assertion

Ref	Expression
simp3i	⊢ 𝜒

Proof of Theorem simp3i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
2		simp3 1156	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
3	1, 2	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  hartogslem2  9501  harwdom  9549  divalglem6  16451  structfn  17211  strleun  17212  oppchomfval  17765  sratset  21304  srads  21306  tngip  24804  dfrelog  26730  log2ub  27114  birthdaylem3  27118  birthday  27119  divsqrtsum2  27147  harmonicbnd2  27169  lgslem4  27464  lgscllem  27468  lgsdir2lem2  27490  lgsdir2lem3  27491  mulog2sumlem1  27698  siilem2  31204  h2hva  31326  h2hsm  31327  h2hnm  31328  elunop2  32365  wallispilem3  46781  wallispilem4  46782  prstchomval  50337  cnelsubclem  50381