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  6773  exmidapne  7472  addcanprleml  7827  addcanprlemu  7828  ltmprr  7855  lelttrdi  8599  ixxdisj  10131  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccss2  10172  iocssre  10181  icossre  10182  iccssre  10183  icodisj  10220  iccf1o  10232  fzen  10271  ioom  10513  intfracq  10575  flqdiv  10576  mulqaddmodid  10619  modsumfzodifsn  10651  addmodlteq  10653  remul  11426  sumtp  11968  crth  12789  phimullem  12790  eulerthlem1  12792  eulerthlemfi  12793  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  ctiunct  13054  strsetsid  13108  strleund  13179  strext  13181  mhmf  13541  submss  13552  eqger  13804  eqgcpbl  13808  lmodvscl  14312  lssssg  14367  rnglidlmsgrp  14504  2idlcpblrng  14530  lmfpm  14960  lmff  14966  lmtopcnp  14967  xmeter  15153  tgqioo  15272  ivthinclemlopn  15353  ivthinclemuopn  15355  limcimolemlt  15381  limcresi  15383  cosordlem  15566  relogbval  15668  relogbzcl  15669  nnlogbexp  15676  perfectlem2  15717  wlkprop  16138  wlkf  16141  wlkfg  16142  wlkvtxiedg  16156  wlk1walkdom  16170  wlkvtxedg  16174  upgr2wlkdc  16186  isclwwlkng  16215  eupthseg  16261