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  7941  hartogslem2  9574  harwdom  9622  divalglem6  16612  structfn  17378  strleun  17379  oppcbas  17942  rescbas  18054  rescabs  18058  rmodislmod  21256  sratset  21509  srads  21511  tngsca  25019  birthday  27339  divsqrsumf  27365  emcl  27387  lgslem4  27684  lgscllem  27688  lgsdir2lem2  27710  mulog2sumlem1  27918  siilem2  31511  h2hva  31633  h2hsm  31634  elunop2  32672  zlmds  34705  zlmtset  34706  wallispilem3  47350  wallispilem4  47351  prstcbas  51023  cnelsubcw  51072  parswapfunc  51109  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114