Theorem simp1i 1157

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

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  find  7894  hartogslem2  9508  harwdom  9556  divalglem6  16473  structfn  17233  strleun  17234  oppcbas  17791  rescbas  17903  rescabs  17907  rmodislmod  21080  sratset  21333  srads  21335  tngsca  24831  birthday  27148  divsqrsumf  27174  emcl  27196  lgslem4  27493  lgscllem  27497  lgsdir2lem2  27519  mulog2sumlem1  27727  siilem2  31233  h2hva  31355  h2hsm  31356  elunop2  32394  zlmds  34375  zlmtset  34376  wallispilem3  46814  wallispilem4  46815  prstcbas  50365  cnelsubclem  50414  rr3fv1cli  50662