Theorem simp3i 1092

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

Syntax hints:   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  hartogslem2  8489  harwdom  8536  divalglem6  15168  structfn  15921  strleun  16019  dfrelog  24357  log2ub  24721  birthdaylem3  24725  birthday  24726  divsqrtsum2  24754  harmonicbnd2  24776  lgslem4  25070  lgscllem  25074  lgsdir2lem2  25096  lgsdir2lem3  25097  mulog2sumlem1  25268  siilem2  27835  h2hva  27959  h2hsm  27960  h2hnm  27961  elunop2  29000  wallispilem3  40602  wallispilem4  40603