Theorem simp1d 1036

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp1bi  1039  erinxp  6845  exmidapne  7579  addcanprleml  7934  addcanprlemu  7935  ltmprr  7962  lelttrdi  8705  ixxdisj  10242  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccss2  10283  iocssre  10292  icossre  10293  iccssre  10294  icodisj  10331  iccf1o  10344  fzen  10383  ioom  10627  intfracq  10689  flqdiv  10690  mulqaddmodid  10733  modsumfzodifsn  10765  addmodlteq  10767  remul  11565  sumtp  12108  crth  12929  phimullem  12930  eulerthlem1  12932  eulerthlemfi  12933  eulerthlemrprm  12934  eulerthlema  12935  eulerthlemh  12936  eulerthlemth  12937  ballotfilemcdc  13150  ballotfilemfc0  13157  ctiunct  13212  strsetsid  13266  strleund  13337  strext  13339  mhmf  13699  submss  13710  eqger  13962  eqgcpbl  13966  lmodvscl  14502  lssssg  14557  rnglidlmsgrp  14694  2idlcpblrng  14720  lmfpm  15157  lmff  15163  lmtopcnp  15164  xmeter  15350  tgqioo  15469  ivthinclemlopn  15550  ivthinclemuopn  15552  limcimolemlt  15578  limcresi  15580  cosordlem  15763  relogbval  15865  relogbzcl  15866  nnlogbexp  15873  perfectlem2  15917  wlkprop  16371  wlkf  16374  wlkfg  16375  wlkvtxiedg  16389  wlk1walkdom  16403  wlkvtxedg  16407  upgr2wlkdc  16421  isclwwlkng  16450  eupthseg  16496  trlsegvdeglem3  16506  trlsegvdeglem5  16508  depindlem2  16551  depindlem3  16552