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

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  9515  harwdom  9563  divalglem6  16488  structfn  17248  strleun  17249  oppchomfval  17802  sratset  21367  srads  21369  tngip  24873  dfrelog  26802  log2ub  27186  birthdaylem3  27190  birthday  27191  divsqrtsum2  27219  harmonicbnd2  27241  lgslem4  27536  lgscllem  27540  lgsdir2lem2  27562  lgsdir2lem3  27563  mulog2sumlem1  27770  siilem2  31333  h2hva  31455  h2hsm  31456  h2hnm  31457  elunop2  32494  wallispilem3  46895  wallispilem4  46896  prstchomval  50485  cnelsubclem  50529