Theorem simp3i 1141

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

Syntax hints:   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  hartogslem2  9446  harwdom  9494  divalglem6  16323  structfn  17081  strleun  17082  oppchomfval  17635  sratset  21133  srads  21135  tngip  24589  dfrelog  26528  log2ub  26913  birthdaylem3  26917  birthday  26918  divsqrtsum2  26947  harmonicbnd2  26969  lgslem4  27265  lgscllem  27269  lgsdir2lem2  27291  lgsdir2lem3  27292  mulog2sumlem1  27499  siilem2  30876  h2hva  30998  h2hsm  30999  h2hnm  31000  elunop2  32037  wallispilem3  46253  wallispilem4  46254  prstchomval  49746  cnelsubclem  49790