Theorem simp3d 995

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 983	. 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  ax-ia2 106  ax-ia3 107

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

This theorem is referenced by:  simp3bi  998  erinxp  6503  resixp  6627  addcanprleml  7422  addcanprlemu  7423  ltmprr  7450  lelttrdi  8188  ixxdisj  9686  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccsupr  9749  icodisj  9775  ioom  10038  intfracq  10093  flqdiv  10094  mulqaddmodid  10137  modsumfzodifsn  10169  cjmul  10657  sumtp  11183  crth  11900  ennnfonelemim  11937  ctiunct  11953  strsetsid  11992  strleund  12047  lmcvg  12386  lmff  12418  lmtopcnp  12419  xmeter  12605  xmetresbl  12609  tgqioo  12716  ivthinclemlopn  12783  ivthinclemuopn  12785  limccl  12797  limcdifap  12800  limcresi  12804  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  cosordlem  12930