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  9512  harwdom  9560  divalglem6  16478  structfn  17238  strleun  17239  oppchomfval  17792  sratset  21354  srads  21356  tngip  24855  dfrelog  26781  log2ub  27165  birthdaylem3  27169  birthday  27170  divsqrtsum2  27198  harmonicbnd2  27220  lgslem4  27515  lgscllem  27519  lgsdir2lem2  27541  lgsdir2lem3  27542  mulog2sumlem1  27749  siilem2  31275  h2hva  31397  h2hsm  31398  h2hnm  31399  elunop2  32436  wallispilem3  46839  wallispilem4  46840  prstchomval  50394  cnelsubclem  50438