Theorem simp1d 1009

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

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

This theorem is referenced by:  simp1bi  1012  erinxp  6604  exmidapne  7254  addcanprleml  7608  addcanprlemu  7609  ltmprr  7636  lelttrdi  8377  ixxdisj  9897  ixxss1  9898  ixxss2  9899  ixxss12  9900  iccss2  9938  iocssre  9947  icossre  9948  iccssre  9949  icodisj  9986  iccf1o  9998  fzen  10036  ioom  10254  intfracq  10313  flqdiv  10314  mulqaddmodid  10357  modsumfzodifsn  10389  addmodlteq  10391  remul  10872  sumtp  11413  crth  12214  phimullem  12215  eulerthlem1  12217  eulerthlemfi  12218  eulerthlemrprm  12219  eulerthlema  12220  eulerthlemh  12221  eulerthlemth  12222  ctiunct  12431  strsetsid  12485  strleund  12552  strext  12554  mhmf  12784  submss  12795  lmfpm  13525  lmff  13531  lmtopcnp  13532  xmeter  13718  tgqioo  13829  ivthinclemlopn  13896  ivthinclemuopn  13898  limcimolemlt  13915  limcresi  13917  cosordlem  14052  relogbval  14151  relogbzcl  14152  nnlogbexp  14159