Theorem simp1d 1040

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  simp1bi  1043  erinxp  6877  exmidapne  7620  addcanprleml  7975  addcanprlemu  7976  ltmprr  8003  lelttrdi  8748  ixxdisj  10288  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccss2  10329  iocssre  10338  icossre  10339  iccssre  10340  icodisj  10377  iccf1o  10390  fzen  10430  ioom  10678  intfracq  10740  flqdiv  10741  mulqaddmodid  10784  modsumfzodifsn  10816  addmodlteq  10818  remul  11620  sumtp  12164  crth  12985  phimullem  12986  eulerthlem1  12988  eulerthlemfi  12989  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  ballotfilemcdc  13206  ballotfilemfc0  13215  ballotfilemro  13249  ctiunct  13314  strsetsid  13368  strleund  13440  strext  13442  mhmf  13755  submss  13766  eqger  14010  eqgcpbl  14014  lmodvscl  14624  lssssg  14680  rnglidlmsgrp  14817  2idlcpblrng  14843  lmfpm  15327  lmff  15333  lmtopcnp  15334  xmeter  15520  tgqioo  15639  ivthinclemlopn  15720  ivthinclemuopn  15722  limcimolemlt  15748  limcresi  15750  cosordlem  15933  relogbval  16036  relogbzcl  16037  nnlogbexp  16044  perfectlem2  16097  wlkprop  16551  wlkf  16554  wlkfg  16555  wlkvtxiedg  16569  wlk1walkdom  16583  wlkvtxedg  16587  upgr2wlkdc  16601  isclwwlkng  16630  eupthseg  16676  trlsegvdeglem3  16686  trlsegvdeglem5  16688  depindlem2  16731  depindlem3  16732