Theorem simp1d 916

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

Syntax hints:   → wi 4   ∧ w3a 885

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

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simp1bi  919  erinxp  6180  addcanprleml  6712  addcanprlemu  6713  ltmprr  6740  lelttrdi  7421  ixxdisj  8772  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  iocssre  8822  icossre  8823  iccssre  8824  icodisj  8860  iccf1o  8872  fzen  8907  intfracq  9162  flqdiv  9163  remul  9472