Theorem simp2d 975

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

Syntax hints:   → wi 4   ∧ w3a 943

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

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

This theorem is referenced by:  simp2bi  978  erinxp  6455  resixp  6579  addcanprleml  7364  addcanprlemu  7365  ltmprr  7392  lelttrdi  8101  ixxdisj  9573  ixxss1  9574  ixxss2  9575  ixxss12  9576  iccgelb  9602  iccss2  9614  icodisj  9662  ioom  9925  flqdiv  9981  mulqaddmodid  10024  modsumfzodifsn  10056  addmodlteq  10058  immul  10538  sumtp  11069  crth  11739  phimullem  11740  ctiunct  11790  structn0fun  11809  strleund  11884  lmcl  12250  lmtopcnp  12255  xmeter  12419  tgqioo  12527  limcimolemlt  12583  limcresi  12585  limccnpcntop  12594  limccnp2lem  12595  limccnp2cntop  12596