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  6783  exmidapne  7484  addcanprleml  7839  addcanprlemu  7840  ltmprr  7867  lelttrdi  8611  ixxdisj  10143  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccss2  10184  iocssre  10193  icossre  10194  iccssre  10195  icodisj  10232  iccf1o  10244  fzen  10283  ioom  10526  intfracq  10588  flqdiv  10589  mulqaddmodid  10632  modsumfzodifsn  10664  addmodlteq  10666  remul  11455  sumtp  11998  crth  12819  phimullem  12820  eulerthlem1  12822  eulerthlemfi  12823  eulerthlemrprm  12824  eulerthlema  12825  eulerthlemh  12826  eulerthlemth  12827  ctiunct  13084  strsetsid  13138  strleund  13209  strext  13211  mhmf  13571  submss  13582  eqger  13834  eqgcpbl  13838  lmodvscl  14343  lssssg  14398  rnglidlmsgrp  14535  2idlcpblrng  14561  lmfpm  14996  lmff  15002  lmtopcnp  15003  xmeter  15189  tgqioo  15308  ivthinclemlopn  15389  ivthinclemuopn  15391  limcimolemlt  15417  limcresi  15419  cosordlem  15602  relogbval  15704  relogbzcl  15705  nnlogbexp  15712  perfectlem2  15753  wlkprop  16207  wlkf  16210  wlkfg  16211  wlkvtxiedg  16225  wlk1walkdom  16239  wlkvtxedg  16243  upgr2wlkdc  16257  isclwwlkng  16286  eupthseg  16332  trlsegvdeglem3  16342  trlsegvdeglem5  16344  depindlem2  16387  depindlem3  16388