Theorem simp2d 994

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 982	. 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

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

This theorem is referenced by:  simp2bi  997  erinxp  6496  resixp  6620  addcanprleml  7415  addcanprlemu  7416  ltmprr  7443  lelttrdi  8181  ixxdisj  9679  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccgelb  9708  iccss2  9720  icodisj  9768  ioom  10031  flqdiv  10087  mulqaddmodid  10130  modsumfzodifsn  10162  addmodlteq  10164  immul  10644  sumtp  11176  crth  11889  phimullem  11890  ctiunct  11942  structn0fun  11961  strleund  12036  lmcl  12403  lmtopcnp  12408  xmeter  12594  tgqioo  12705  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimolemlt  12791  limcresi  12793  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  cosordlem  12919