Theorem simp3i 1147

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

Syntax hints:   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  hartogslem2  9448  harwdom  9496  divalglem6  16358  structfn  17117  strleun  17118  oppchomfval  17671  sratset  21173  srads  21175  tngip  24630  dfrelog  26547  log2ub  26931  birthdaylem3  26935  birthday  26936  divsqrtsum2  26964  harmonicbnd2  26986  lgslem4  27281  lgscllem  27285  lgsdir2lem2  27307  lgsdir2lem3  27308  mulog2sumlem1  27515  siilem2  30941  h2hva  31063  h2hsm  31064  h2hnm  31065  elunop2  32102  wallispilem3  46510  wallispilem4  46511  prstchomval  50049  cnelsubclem  50093