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  6856  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8718  ixxdisj  10258  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccss2  10299  iocssre  10308  icossre  10309  iccssre  10310  icodisj  10347  iccf1o  10360  fzen  10400  ioom  10647  intfracq  10709  flqdiv  10710  mulqaddmodid  10753  modsumfzodifsn  10785  addmodlteq  10787  remul  11585  sumtp  12128  crth  12949  phimullem  12950  eulerthlem1  12952  eulerthlemfi  12953  eulerthlemrprm  12954  eulerthlema  12955  eulerthlemh  12956  eulerthlemth  12957  ballotfilemcdc  13170  ballotfilemfc0  13179  ballotfilemro  13213  ctiunct  13278  strsetsid  13332  strleund  13403  strext  13405  mhmf  13723  submss  13734  eqger  13980  eqgcpbl  13984  lmodvscl  14582  lssssg  14637  rnglidlmsgrp  14774  2idlcpblrng  14800  lmfpm  15237  lmff  15243  lmtopcnp  15244  xmeter  15430  tgqioo  15549  ivthinclemlopn  15630  ivthinclemuopn  15632  limcimolemlt  15658  limcresi  15660  cosordlem  15843  relogbval  15945  relogbzcl  15946  nnlogbexp  15953  perfectlem2  15997  wlkprop  16451  wlkf  16454  wlkfg  16455  wlkvtxiedg  16469  wlk1walkdom  16483  wlkvtxedg  16487  upgr2wlkdc  16501  isclwwlkng  16530  eupthseg  16576  trlsegvdeglem3  16586  trlsegvdeglem5  16588  depindlem2  16631  depindlem3  16632