Theorem simp1i 1139

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

Syntax hints:   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  find  7837  hartogslem2  9448  harwdom  9496  divalglem6  16325  structfn  17083  strleun  17084  oppcbas  17641  rescbas  17753  rescabs  17757  rmodislmod  20881  sratset  21135  srads  21137  tngsca  24589  birthday  26920  divsqrsumf  26947  emcl  26969  lgslem4  27267  lgscllem  27271  lgsdir2lem2  27293  mulog2sumlem1  27501  siilem2  30927  h2hva  31049  h2hsm  31050  elunop2  32088  zlmds  34119  zlmtset  34120  wallispilem3  46311  wallispilem4  46312  prstcbas  49799  cnelsubclem  49848