Theorem simp2d 1010

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

Syntax hints:   → wi 4   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simp2bi  1013  erinxp  6599  resixp  6723  addcanprleml  7588  addcanprlemu  7589  ltmprr  7616  lelttrdi  8357  ixxdisj  9872  ixxss1  9873  ixxss2  9874  ixxss12  9875  iccgelb  9901  iccss2  9913  icodisj  9961  ioom  10229  elicore  10235  flqdiv  10289  mulqaddmodid  10332  modsumfzodifsn  10364  addmodlteq  10366  immul  10854  sumtp  11388  crth  12189  phimullem  12190  eulerthlem1  12192  eulerthlema  12195  eulerthlemh  12196  eulerthlemth  12197  ctiunct  12406  structn0fun  12440  strleund  12517  mhmlin  12719  subm0cl  12729  lmcl  13296  lmtopcnp  13301  xmeter  13487  tgqioo  13598  ivthinclemlopn  13665  ivthinclemuopn  13667  limcimolemlt  13684  limcresi  13686  limccnpcntop  13695  limccnp2lem  13696  limccnp2cntop  13697  cosordlem  13821