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 1087

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 1089

This theorem is referenced by:  find  7838  findOLD  7839  hartogslem2  9488  harwdom  9536  divalglem6  16291  structfn  17039  strleun  17040  oppcbas  17613  rescbas  17726  rescabs  17732  rmodislmod  20447  rmodislmodOLD  20448  sratset  20710  srads  20713  tngsca  24042  birthday  26341  divsqrsumf  26367  emcl  26389  lgslem4  26685  lgscllem  26689  lgsdir2lem2  26711  mulog2sumlem1  26919  siilem2  29857  h2hva  29979  h2hsm  29980  elunop2  31018  zlmds  32632  zlmtset  32634  wallispilem3  44428  wallispilem4  44429  prstcbas  47207