Theorem simp3d 963

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

Syntax hints:   → wi 4   ∧ w3a 930

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

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

This theorem is referenced by:  simp3bi  966  erinxp  6433  resixp  6557  addcanprleml  7323  addcanprlemu  7324  ltmprr  7351  lelttrdi  8055  ixxdisj  9527  ixxss1  9528  ixxss2  9529  ixxss12  9530  iccsupr  9590  icodisj  9616  ioom  9879  intfracq  9934  flqdiv  9935  mulqaddmodid  9978  modsumfzodifsn  10010  cjmul  10498  sumtp  11022  crth  11692  ennnfonelemim  11729  strsetsid  11774  strleund  11829  lmcvg  12167  lmff  12199  lmtopcnp  12200  xmeter  12364  xmetresbl  12368  tgqioo  12466  limccl  12510  limcdifap  12512  limcresi  12515  limccnpcntop  12520