Theorem simp3i 1072

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

Syntax hints:   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  hartogslem2  8448  harwdom  8495  divalglem6  15121  structfn  15874  strleun  15972  dfrelog  24312  log2ub  24676  birthdaylem3  24680  birthday  24681  divsqrtsum2  24709  harmonicbnd2  24731  lgslem4  25025  lgscllem  25029  lgsdir2lem2  25051  lgsdir2lem3  25052  mulog2sumlem1  25223  siilem2  27707  h2hva  27831  h2hsm  27832  h2hnm  27833  elunop2  28872  wallispilem3  40284  wallispilem4  40285