Theorem simp1i 1138

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 1135	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  find  7752  findOLD  7753  hartogslem2  9311  harwdom  9359  divalglem6  16116  structfn  16866  strleun  16867  oppcbas  17437  rescbas  17550  rescabs  17556  rmodislmod  20200  rmodislmodOLD  20201  sratset  20461  srads  20464  tngsca  23814  birthday  26113  divsqrsumf  26139  emcl  26161  lgslem4  26457  lgscllem  26461  lgsdir2lem2  26483  mulog2sumlem1  26691  siilem2  29223  h2hva  29345  h2hsm  29346  elunop2  30384  zlmds  31921  zlmtset  31923  wallispilem3  43615  wallispilem4  43616  prstcbas  46359