Theorem simp3i 1175

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

Syntax hints:   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  hartogslem2  8724  harwdom  8771  divalglem6  15502  structfn  16246  strleun  16338  dfrelog  24718  log2ub  25096  birthdaylem3  25100  birthday  25101  divsqrtsum2  25129  harmonicbnd2  25151  lgslem4  25445  lgscllem  25449  lgsdir2lem2  25471  lgsdir2lem3  25472  mulog2sumlem1  25643  siilem2  28258  h2hva  28382  h2hsm  28383  h2hnm  28384  elunop2  29423  wallispilem3  41072  wallispilem4  41073