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  7908  hartogslem2  9541  harwdom  9589  divalglem6  16574  structfn  17340  strleun  17341  oppcbas  17898  rescbas  18010  rescabs  18014  rmodislmod  21211  sratset  21464  srads  21466  tngsca  24970  birthday  27288  divsqrsumf  27314  emcl  27336  lgslem4  27633  lgscllem  27637  lgsdir2lem2  27659  mulog2sumlem1  27867  siilem2  31460  h2hva  31582  h2hsm  31583  elunop2  32621  zlmds  34641  zlmtset  34642  wallispilem3  47171  wallispilem4  47172  prstcbas  50786  cnelsubcw  50835  parswapfunc  50872  par2diag  50874  fuconuniqlem  50875  fuconuniqvalslem  50877