Theorem simp1d 1035

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp1bi  1038  erinxp  6778  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iocssre  10188  icossre  10189  iccssre  10190  icodisj  10227  iccf1o  10239  fzen  10278  ioom  10521  intfracq  10583  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  addmodlteq  10661  remul  11434  sumtp  11977  crth  12798  phimullem  12799  eulerthlem1  12801  eulerthlemfi  12802  eulerthlemrprm  12803  eulerthlema  12804  eulerthlemh  12805  eulerthlemth  12806  ctiunct  13063  strsetsid  13117  strleund  13188  strext  13190  mhmf  13550  submss  13561  eqger  13813  eqgcpbl  13817  lmodvscl  14322  lssssg  14377  rnglidlmsgrp  14514  2idlcpblrng  14540  lmfpm  14970  lmff  14976  lmtopcnp  14977  xmeter  15163  tgqioo  15282  ivthinclemlopn  15363  ivthinclemuopn  15365  limcimolemlt  15391  limcresi  15393  cosordlem  15576  relogbval  15678  relogbzcl  15679  nnlogbexp  15686  perfectlem2  15727  wlkprop  16181  wlkf  16184  wlkfg  16185  wlkvtxiedg  16199  wlk1walkdom  16213  wlkvtxedg  16217  upgr2wlkdc  16231  isclwwlkng  16260  eupthseg  16306  trlsegvdeglem3  16316  trlsegvdeglem5  16318  depindlem2  16347  depindlem3  16348