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 ⊢ 𝜑

Syntax hints:   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  find  7893  hartogslem2  9506  harwdom  9554  divalglem6  16457  structfn  17217  strleun  17218  oppcbas  17775  rescbas  17887  rescabs  17891  rmodislmod  21032  sratset  21285  srads  21287  tngsca  24783  birthday  27100  divsqrsumf  27126  emcl  27148  lgslem4  27445  lgscllem  27449  lgsdir2lem2  27471  mulog2sumlem1  27679  siilem2  31185  h2hva  31307  h2hsm  31308  elunop2  32346  zlmds  34333  zlmtset  34334  wallispilem3  46764  wallispilem4  46765  prstcbas  50315  cnelsubclem  50364