Theorem simp3d 953

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

Hypothesis

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

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

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

Syntax hints:   → wi 4   ∧ w3a 920

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

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

This theorem is referenced by:  simp3bi  956  erinxp  6296  addcanprleml  7076  addcanprlemu  7077  ltmprr  7104  lelttrdi  7807  ixxdisj  9216  ixxss1  9217  ixxss2  9218  ixxss12  9219  iccsupr  9279  icodisj  9304  ioom  9561  intfracq  9616  flqdiv  9617  mulqaddmodid  9660  modsumfzodifsn  9692  cjmul  10146  crth  10980