Theorem simp1i 1136

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

Syntax hints:   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  find  7587  findOLD  7588  hartogslem2  8991  harwdom  9039  divalglem6  15739  structfn  16492  strleun  16583  rmodislmod  19695  birthday  25540  divsqrsumf  25566  emcl  25588  lgslem4  25884  lgscllem  25888  lgsdir2lem2  25910  mulog2sumlem1  26118  siilem2  28635  h2hva  28757  h2hsm  28758  elunop2  29796  wallispilem3  42709  wallispilem4  42710