Theorem simp1i 1135

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 1132	. 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:  find  7609  hartogslem2  9009  harwdom  9056  divalglem6  15751  structfn  16502  strleun  16593  rmodislmod  19704  birthday  25534  divsqrsumf  25560  emcl  25582  lgslem4  25878  lgscllem  25882  lgsdir2lem2  25904  mulog2sumlem1  26112  siilem2  28631  h2hva  28753  h2hsm  28754  elunop2  29792  wallispilem3  42359  wallispilem4  42360