Theorem simp1d 1009

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	|- ( ph -> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
simp1d	|- ( ph -> ps )

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp1 997	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  simp1bi  1012  erinxp  6611  exmidapne  7261  addcanprleml  7615  addcanprlemu  7616  ltmprr  7643  lelttrdi  8385  ixxdisj  9905  ixxss1  9906  ixxss2  9907  ixxss12  9908  iccss2  9946  iocssre  9955  icossre  9956  iccssre  9957  icodisj  9994  iccf1o  10006  fzen  10045  ioom  10263  intfracq  10322  flqdiv  10323  mulqaddmodid  10366  modsumfzodifsn  10398  addmodlteq  10400  remul  10883  sumtp  11424  crth  12226  phimullem  12227  eulerthlem1  12229  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  ctiunct  12443  strsetsid  12497  strleund  12564  strext  12566  mhmf  12861  submss  12872  eqger  13088  eqgcpbl  13092  lmodvscl  13400  lssssg  13452  lmfpm  13782  lmff  13788  lmtopcnp  13789  xmeter  13975  tgqioo  14086  ivthinclemlopn  14153  ivthinclemuopn  14155  limcimolemlt  14172  limcresi  14174  cosordlem  14309  relogbval  14408  relogbzcl  14409  nnlogbexp  14416