Theorem simp1d 976

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

Syntax hints:   → wi 4   ∧ w3a 945

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

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

This theorem is referenced by:  simp1bi  979  erinxp  6457  addcanprleml  7370  addcanprlemu  7371  ltmprr  7398  lelttrdi  8107  ixxdisj  9579  ixxss1  9580  ixxss2  9581  ixxss12  9582  iccss2  9620  iocssre  9629  icossre  9630  iccssre  9631  icodisj  9668  iccf1o  9680  fzen  9716  ioom  9931  intfracq  9986  flqdiv  9987  mulqaddmodid  10030  modsumfzodifsn  10062  addmodlteq  10064  remul  10537  sumtp  11075  crth  11745  phimullem  11746  ctiunct  11796  strsetsid  11835  strleund  11890  lmfpm  12254  lmff  12260  lmtopcnp  12261  xmeter  12425  tgqioo  12533  limcimolemlt  12589  limcresi  12591