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 1086

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 1088

This theorem is referenced by:  hartogslem2  9472  harwdom  9520  divalglem6  16344  structfn  17102  strleun  17103  oppchomfval  17651  sratset  21066  srads  21068  tngip  24511  dfrelog  26450  log2ub  26835  birthdaylem3  26839  birthday  26840  divsqrtsum2  26869  harmonicbnd2  26891  lgslem4  27187  lgscllem  27191  lgsdir2lem2  27213  lgsdir2lem3  27214  mulog2sumlem1  27421  siilem2  30754  h2hva  30876  h2hsm  30877  h2hnm  30878  elunop2  31915  wallispilem3  46038  wallispilem4  46039  prstchomval  49521  cnelsubclem  49565