Theorem simp3i 1141

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 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
3	1, 2	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  hartogslem2  9612  harwdom  9660  divalglem6  16446  structfn  17203  strleun  17204  oppchomfval  17772  sratset  21211  srads  21214  tngip  24687  dfrelog  26625  log2ub  27010  birthdaylem3  27014  birthday  27015  divsqrtsum2  27044  harmonicbnd2  27066  lgslem4  27362  lgscllem  27366  lgsdir2lem2  27388  lgsdir2lem3  27389  mulog2sumlem1  27596  siilem2  30884  h2hva  31006  h2hsm  31007  h2hnm  31008  elunop2  32045  wallispilem3  45988  wallispilem4  45989  prstchomval  48741