Theorem simp3i 1138

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

Syntax hints:   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  hartogslem2  8991  harwdom  9039  divalglem6  15739  structfn  16492  strleun  16583  dfrelog  25157  log2ub  25535  birthdaylem3  25539  birthday  25540  divsqrtsum2  25568  harmonicbnd2  25590  lgslem4  25884  lgscllem  25888  lgsdir2lem2  25910  lgsdir2lem3  25911  mulog2sumlem1  26118  siilem2  28635  h2hva  28757  h2hsm  28758  h2hnm  28759  elunop2  29796  wallispilem3  42709  wallispilem4  42710