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  9544  harwdom  9592  divalglem6  16577  structfn  17343  strleun  17344  oppchomfval  17897  sratset  21467  srads  21469  tngip  24975  dfrelog  26902  log2ub  27286  birthdaylem3  27290  birthday  27291  divsqrtsum2  27319  harmonicbnd2  27341  lgslem4  27636  lgscllem  27640  lgsdir2lem2  27662  lgsdir2lem3  27663  mulog2sumlem1  27870  siilem2  31463  h2hva  31585  h2hsm  31586  h2hnm  31587  elunop2  32624  wallispilem3  47185  wallispilem4  47186  prstchomval  50805  cnelsubcw  50849  par2diag  50888  fuconuniqlem  50889  fuconuniqvalslem  50891