Theorem simp1d 1014

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

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  simp1bi  1017  erinxp  6726  exmidapne  7414  addcanprleml  7769  addcanprlemu  7770  ltmprr  7797  lelttrdi  8541  ixxdisj  10067  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccss2  10108  iocssre  10117  icossre  10118  iccssre  10119  icodisj  10156  iccf1o  10168  fzen  10207  ioom  10447  intfracq  10509  flqdiv  10510  mulqaddmodid  10553  modsumfzodifsn  10585  addmodlteq  10587  remul  11349  sumtp  11891  crth  12712  phimullem  12713  eulerthlem1  12715  eulerthlemfi  12716  eulerthlemrprm  12717  eulerthlema  12718  eulerthlemh  12719  eulerthlemth  12720  ctiunct  12977  strsetsid  13031  strleund  13102  strext  13104  mhmf  13464  submss  13475  eqger  13727  eqgcpbl  13731  lmodvscl  14234  lssssg  14289  rnglidlmsgrp  14426  2idlcpblrng  14452  lmfpm  14882  lmff  14888  lmtopcnp  14889  xmeter  15075  tgqioo  15194  ivthinclemlopn  15275  ivthinclemuopn  15277  limcimolemlt  15303  limcresi  15305  cosordlem  15488  relogbval  15590  relogbzcl  15591  nnlogbexp  15598  perfectlem2  15639