Theorem simp3i 1137

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

Syntax hints:   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  hartogslem2  9010  harwdom  9057  divalglem6  15752  structfn  16503  strleun  16594  dfrelog  25152  log2ub  25530  birthdaylem3  25534  birthday  25535  divsqrtsum2  25563  harmonicbnd2  25585  lgslem4  25879  lgscllem  25883  lgsdir2lem2  25905  lgsdir2lem3  25906  mulog2sumlem1  26113  siilem2  28632  h2hva  28754  h2hsm  28755  h2hnm  28756  elunop2  29793  wallispilem3  42359  wallispilem4  42360