Theorem simp1i 1070

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

Syntax hints:   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  find  7091  hartogslem2  8448  harwdom  8495  divalglem6  15121  structfn  15874  strleun  15972  rmodislmod  18931  birthday  24681  divsqrsumf  24707  emcl  24729  lgslem4  25025  lgscllem  25029  lgsdir2lem2  25051  mulog2sumlem1  25223  siilem2  27707  h2hva  27831  h2hsm  27832  elunop2  28872  wallispilem3  40284  wallispilem4  40285