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  9503  harwdom  9551  divalglem6  16375  structfn  17133  strleun  17134  oppchomfval  17682  sratset  21097  srads  21099  tngip  24542  dfrelog  26481  log2ub  26866  birthdaylem3  26870  birthday  26871  divsqrtsum2  26900  harmonicbnd2  26922  lgslem4  27218  lgscllem  27222  lgsdir2lem2  27244  lgsdir2lem3  27245  mulog2sumlem1  27452  siilem2  30788  h2hva  30910  h2hsm  30911  h2hnm  30912  elunop2  31949  wallispilem3  46072  wallispilem4  46073  prstchomval  49552  cnelsubclem  49596