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  6496  addcanprleml  7415  addcanprlemu  7416  ltmprr  7443  lelttrdi  8181  ixxdisj  9679  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccss2  9720  iocssre  9729  icossre  9730  iccssre  9731  icodisj  9768  iccf1o  9780  fzen  9816  ioom  10031  intfracq  10086  flqdiv  10087  mulqaddmodid  10130  modsumfzodifsn  10162  addmodlteq  10164  remul  10637  sumtp  11176  crth  11889  phimullem  11890  ctiunct  11942  strsetsid  11981  strleund  12036  lmfpm  12401  lmff  12407  lmtopcnp  12408  xmeter  12594  tgqioo  12705  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimolemlt  12791  limcresi  12793  cosordlem  12919