Theorem simp1d 994

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

Hypothesis

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

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 982	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 963

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

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

This theorem is referenced by:  simp1bi  997  erinxp  6543  addcanprleml  7513  addcanprlemu  7514  ltmprr  7541  lelttrdi  8280  ixxdisj  9785  ixxss1  9786  ixxss2  9787  ixxss12  9788  iccss2  9826  iocssre  9835  icossre  9836  iccssre  9837  icodisj  9874  iccf1o  9886  fzen  9923  ioom  10138  intfracq  10197  flqdiv  10198  mulqaddmodid  10241  modsumfzodifsn  10273  addmodlteq  10275  remul  10749  sumtp  11288  crth  12068  phimullem  12069  eulerthlem1  12071  eulerthlemfi  12072  eulerthlemrprm  12073  eulerthlema  12074  eulerthlemh  12075  eulerthlemth  12076  ctiunct  12128  strsetsid  12170  strleund  12225  lmfpm  12590  lmff  12596  lmtopcnp  12597  xmeter  12783  tgqioo  12894  ivthinclemlopn  12961  ivthinclemuopn  12963  limcimolemlt  12980  limcresi  12982  cosordlem  13117  relogbval  13215  relogbzcl  13216  nnlogbexp  13223