Theorem simp3d 1000

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

Syntax hints:   → wi 4   ∧ w3a 967

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 969

This theorem is referenced by:  simp3bi  1003  erinxp  6566  resixp  6690  addcanprleml  7546  addcanprlemu  7547  ltmprr  7574  lelttrdi  8315  ixxdisj  9830  ixxss1  9831  ixxss2  9832  ixxss12  9833  iccsupr  9893  icodisj  9919  ioom  10186  elicore  10192  intfracq  10245  flqdiv  10246  mulqaddmodid  10289  modsumfzodifsn  10321  cjmul  10813  sumtp  11341  crth  12133  eulerthlem1  12136  eulerthlemh  12140  eulerthlemth  12141  ennnfonelemim  12294  ctiunct  12310  strsetsid  12364  strleund  12419  lmcvg  12758  lmff  12790  lmtopcnp  12791  xmeter  12977  xmetresbl  12981  tgqioo  13088  ivthinclemlopn  13155  ivthinclemuopn  13157  limccl  13169  limcdifap  13172  limcresi  13176  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  limccoap  13188  cosordlem  13311  relogbval  13410  relogbzcl  13411  nnlogbexp  13418