Theorem simp3i 1157

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 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
3	1, 2	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   ∧ w3a 1101

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 1103

This theorem is referenced by:  hartogslem2  9504  harwdom  9552  divalglem6  16455  structfn  17215  strleun  17216  oppchomfval  17769  sratset  21281  srads  21283  tngip  24772  dfrelog  26695  log2ub  27079  birthdaylem3  27083  birthday  27084  divsqrtsum2  27112  harmonicbnd2  27134  lgslem4  27429  lgscllem  27433  lgsdir2lem2  27455  lgsdir2lem3  27456  mulog2sumlem1  27663  siilem2  31144  h2hva  31266  h2hsm  31267  h2hnm  31268  elunop2  32305  wallispilem3  46672  wallispilem4  46673  prstchomval  50221  cnelsubclem  50265