Theorem simp1d 1033

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp1bi  1036  erinxp  6764  exmidapne  7454  addcanprleml  7809  addcanprlemu  7810  ltmprr  7837  lelttrdi  8581  ixxdisj  10107  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccss2  10148  iocssre  10157  icossre  10158  iccssre  10159  icodisj  10196  iccf1o  10208  fzen  10247  ioom  10488  intfracq  10550  flqdiv  10551  mulqaddmodid  10594  modsumfzodifsn  10626  addmodlteq  10628  remul  11391  sumtp  11933  crth  12754  phimullem  12755  eulerthlem1  12757  eulerthlemfi  12758  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  ctiunct  13019  strsetsid  13073  strleund  13144  strext  13146  mhmf  13506  submss  13517  eqger  13769  eqgcpbl  13773  lmodvscl  14277  lssssg  14332  rnglidlmsgrp  14469  2idlcpblrng  14495  lmfpm  14925  lmff  14931  lmtopcnp  14932  xmeter  15118  tgqioo  15237  ivthinclemlopn  15318  ivthinclemuopn  15320  limcimolemlt  15346  limcresi  15348  cosordlem  15531  relogbval  15633  relogbzcl  15634  nnlogbexp  15641  perfectlem2  15682  wlkprop  16048  wlkf  16051  wlkfg  16052  wlkvtxiedg  16066  wlk1walkdom  16080  wlkvtxedg  16084  upgr2wlkdc  16096