Theorem simp1i 1173

Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis

Ref	Expression
3simp1i.1	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Assertion

Ref	Expression
simp1i	⊢ 𝜑

Proof of Theorem simp1i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
2		simp1 1170	. 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:  find  7357  hartogslem2  8724  harwdom  8771  divalglem6  15502  structfn  16246  strleun  16338  rmodislmod  19294  birthday  25101  divsqrsumf  25127  emcl  25149  lgslem4  25445  lgscllem  25449  lgsdir2lem2  25471  mulog2sumlem1  25643  siilem2  28258  h2hva  28382  h2hsm  28383  elunop2  29423  wallispilem3  41072  wallispilem4  41073