Theorem simp3i 1070

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

Syntax hints:   ∧ w3a 1036

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 386  df-3an 1038

This theorem is referenced by:  hartogslem2  8393  harwdom  8440  divalglem6  15040  structfn  15792  strleun  15888  dfrelog  24211  log2ub  24571  birthdaylem3  24575  birthday  24576  divsqrtsum2  24604  harmonicbnd2  24626  lgslem4  24920  lgscllem  24924  lgsdir2lem2  24946  lgsdir2lem3  24947  mulog2sumlem1  25118  siilem2  27547  h2hva  27671  h2hsm  27672  h2hnm  27673  elunop2  28712  wallispilem3  39559  wallispilem4  39560