Theorem simp3i 1140

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 1137	. 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  9581  harwdom  9629  divalglem6  16432  structfn  17190  strleun  17191  oppchomfval  17759  sratset  21206  srads  21209  tngip  24682  dfrelog  26622  log2ub  27007  birthdaylem3  27011  birthday  27012  divsqrtsum2  27041  harmonicbnd2  27063  lgslem4  27359  lgscllem  27363  lgsdir2lem2  27385  lgsdir2lem3  27386  mulog2sumlem1  27593  siilem2  30881  h2hva  31003  h2hsm  31004  h2hnm  31005  elunop2  32042  wallispilem3  46023  wallispilem4  46024  prstchomval  48875