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  6609  exmidapne  7259  addcanprleml  7613  addcanprlemu  7614  ltmprr  7641  lelttrdi  8383  ixxdisj  9903  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccss2  9944  iocssre  9953  icossre  9954  iccssre  9955  icodisj  9992  iccf1o  10004  fzen  10043  ioom  10261  intfracq  10320  flqdiv  10321  mulqaddmodid  10364  modsumfzodifsn  10396  addmodlteq  10398  remul  10881  sumtp  11422  crth  12224  phimullem  12225  eulerthlem1  12227  eulerthlemfi  12228  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  ctiunct  12441  strsetsid  12495  strleund  12562  strext  12564  mhmf  12856  submss  12867  eqger  13083  eqgcpbl  13087  lmodvscl  13395  lmfpm  13746  lmff  13752  lmtopcnp  13753  xmeter  13939  tgqioo  14050  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimolemlt  14136  limcresi  14138  cosordlem  14273  relogbval  14372  relogbzcl  14373  nnlogbexp  14380