Theorem simp1i 1145

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

Syntax hints:   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  find  7842  hartogslem2  9455  harwdom  9503  divalglem6  16365  structfn  17124  strleun  17125  oppcbas  17682  rescbas  17794  rescabs  17798  rmodislmod  20927  sratset  21180  srads  21182  tngsca  24635  birthday  26943  divsqrsumf  26969  emcl  26991  lgslem4  27288  lgscllem  27292  lgsdir2lem2  27314  mulog2sumlem1  27522  siilem2  30948  h2hva  31070  h2hsm  31071  elunop2  32109  zlmds  34153  zlmtset  34154  wallispilem3  46517  wallispilem4  46518  prstcbas  50051  cnelsubclem  50100