Theorem simp3i 1065

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

Syntax hints:   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  hartogslem2  8331  harwdom  8378  divalglem6  14959  structfn  15708  strleun  15799  dfrelog  24116  log2ub  24476  birthdaylem3  24480  birthday  24481  divsqrtsum2  24509  harmonicbnd2  24531  lgslem4  24825  lgscllem  24829  lgsdir2lem2  24851  lgsdir2lem3  24852  mulog2sumlem1  25023  siilem2  27091  h2hva  27215  h2hsm  27216  h2hnm  27217  elunop2  28256  wallispilem3  38960  wallispilem4  38961