Theorem simp1i 1157

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

This proof depends on syntax axioms:   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  find  7892  hartogslem2  9515  harwdom  9563  divalglem6  16488  structfn  17248  strleun  17249  oppcbas  17806  rescbas  17918  rescabs  17922  rmodislmod  21114  sratset  21367  srads  21369  tngsca  24871  birthday  27191  divsqrsumf  27217  emcl  27239  lgslem4  27536  lgscllem  27540  lgsdir2lem2  27562  mulog2sumlem1  27770  siilem2  31333  h2hva  31455  h2hsm  31456  elunop2  32494  zlmds  34472  zlmtset  34473  wallispilem3  46895  wallispilem4  46896  prstcbas  50480  cnelsubclem  50529