Theorem simp3i 1154

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

Syntax hints:   ∧ w3a 1098

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

This theorem is referenced by:  hartogslem2  9491  harwdom  9539  divalglem6  16432  structfn  17192  strleun  17193  oppchomfval  17746  sratset  21247  srads  21249  tngip  24704  dfrelog  26627  log2ub  27011  birthdaylem3  27015  birthday  27016  divsqrtsum2  27044  harmonicbnd2  27066  lgslem4  27361  lgscllem  27365  lgsdir2lem2  27387  lgsdir2lem3  27388  mulog2sumlem1  27595  siilem2  31052  h2hva  31174  h2hsm  31175  h2hnm  31176  elunop2  32213  wallispilem3  46638  wallispilem4  46639  prstchomval  50177  cnelsubclem  50221