Theorem simp1d 950

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 938	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simp1bi  953  erinxp  6203  addcanprleml  6804  addcanprlemu  6805  ltmprr  6832  lelttrdi  7530  ixxdisj  8926  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccss2  8967  iocssre  8976  icossre  8977  iccssre  8978  icodisj  9014  iccf1o  9026  fzen  9062  ioom  9269  intfracq  9322  flqdiv  9323  mulqaddmodid  9366  modsumfzodifsn  9398  addmodlteq  9400  remul  9759