Theorem simp1d 993

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 981	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simp1bi  996  erinxp  6503  addcanprleml  7429  addcanprlemu  7430  ltmprr  7457  lelttrdi  8195  ixxdisj  9693  ixxss1  9694  ixxss2  9695  ixxss12  9696  iccss2  9734  iocssre  9743  icossre  9744  iccssre  9745  icodisj  9782  iccf1o  9794  fzen  9830  ioom  10045  intfracq  10100  flqdiv  10101  mulqaddmodid  10144  modsumfzodifsn  10176  addmodlteq  10178  remul  10651  sumtp  11190  crth  11907  phimullem  11908  ctiunct  11960  strsetsid  12002  strleund  12057  lmfpm  12422  lmff  12428  lmtopcnp  12429  xmeter  12615  tgqioo  12726  ivthinclemlopn  12793  ivthinclemuopn  12795  limcimolemlt  12812  limcresi  12814  cosordlem  12940