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  9530  harwdom  9578  divalglem6  16561  structfn  17327  strleun  17328  oppchomfval  17881  sratset  21451  srads  21453  tngip  24959  dfrelog  26886  log2ub  27270  birthdaylem3  27274  birthday  27275  divsqrtsum2  27303  harmonicbnd2  27325  lgslem4  27620  lgscllem  27624  lgsdir2lem2  27646  lgsdir2lem3  27647  mulog2sumlem1  27854  siilem2  31447  h2hva  31569  h2hsm  31570  h2hnm  31571  elunop2  32608  wallispilem3  47046  wallispilem4  47047  prstchomval  50636  cnelsubclem  50680