Theorem simp1i 1151

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

Syntax hints:   ∧ w3a 1097

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

This theorem is referenced by:  find  7870  hartogslem2  9484  harwdom  9532  divalglem6  16422  structfn  17182  strleun  17183  oppcbas  17740  rescbas  17852  rescabs  17856  rmodislmod  20984  sratset  21237  srads  21239  tngsca  24692  birthday  27006  divsqrsumf  27032  emcl  27054  lgslem4  27351  lgscllem  27355  lgsdir2lem2  27377  mulog2sumlem1  27585  siilem2  31011  h2hva  31133  h2hsm  31134  elunop2  32172  zlmds  34219  zlmtset  34220  wallispilem3  46601  wallispilem4  46602  prstcbas  50135  cnelsubclem  50184