Theorem simp3i 1142

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

Syntax hints:   ∧ w3a 1087

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 1089

This theorem is referenced by:  hartogslem2  9452  harwdom  9500  divalglem6  16361  structfn  17120  strleun  17121  oppchomfval  17674  sratset  21173  srads  21175  tngip  24625  dfrelog  26545  log2ub  26929  birthdaylem3  26933  birthday  26934  divsqrtsum2  26963  harmonicbnd2  26985  lgslem4  27280  lgscllem  27284  lgsdir2lem2  27306  lgsdir2lem3  27307  mulog2sumlem1  27514  siilem2  30941  h2hva  31063  h2hsm  31064  h2hnm  31065  elunop2  32102  wallispilem3  46516  wallispilem4  46517  prstchomval  50049  cnelsubclem  50093