Theorem simp3i 1159

Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)

Hypothesis

Ref	Expression
3simp1i.1	⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)

Assertion

Ref	Expression
simp3i	⊢ 𝜒

Proof of Theorem simp3i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
2		simp3 1156	. 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:  hartogslem2  9574  harwdom  9622  divalglem6  16612  structfn  17378  strleun  17379  oppchomfval  17938  sratset  21509  srads  21511  tngip  25021  dfrelog  26950  log2ub  27334  birthdaylem3  27338  birthday  27339  divsqrtsum2  27367  harmonicbnd2  27389  lgslem4  27684  lgscllem  27688  lgsdir2lem2  27710  lgsdir2lem3  27711  mulog2sumlem1  27918  siilem2  31511  h2hva  31633  h2hsm  31634  h2hnm  31635  elunop2  32672  wallispilem3  47350  wallispilem4  47351  prstchomval  51028  cnelsubcw  51072  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114