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

This theorem is referenced by:  find  7918  hartogslem2  9581  harwdom  9629  divalglem6  16432  structfn  17190  strleun  17191  oppcbas  17764  rescbas  17877  rescabs  17883  rmodislmod  20945  rmodislmodOLD  20946  sratset  21206  srads  21209  tngsca  24678  birthday  27012  divsqrsumf  27039  emcl  27061  lgslem4  27359  lgscllem  27363  lgsdir2lem2  27385  mulog2sumlem1  27593  siilem2  30881  h2hva  31003  h2hsm  31004  elunop2  32042  zlmds  33923  zlmtset  33925  wallispilem3  46023  wallispilem4  46024  prstcbas  48868