Theorem simp2d 999

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

Hypothesis

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

Assertion

Ref	Expression
simp2d	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp2 987	. 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

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

This theorem is referenced by:  simp2bi  1002  erinxp  6566  resixp  6690  addcanprleml  7546  addcanprlemu  7547  ltmprr  7574  lelttrdi  8315  ixxdisj  9830  ixxss1  9831  ixxss2  9832  ixxss12  9833  iccgelb  9859  iccss2  9871  icodisj  9919  ioom  10186  elicore  10192  flqdiv  10246  mulqaddmodid  10289  modsumfzodifsn  10321  addmodlteq  10323  immul  10807  sumtp  11341  crth  12133  phimullem  12134  eulerthlem1  12136  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  ctiunct  12310  structn0fun  12344  strleund  12419  lmcl  12786  lmtopcnp  12791  xmeter  12977  tgqioo  13088  ivthinclemlopn  13155  ivthinclemuopn  13157  limcimolemlt  13174  limcresi  13176  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  cosordlem  13311