Theorem simp1d 993

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 981	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simp1bi  996  erinxp  6503  addcanprleml  7422  addcanprlemu  7423  ltmprr  7450  lelttrdi  8188  ixxdisj  9686  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccss2  9727  iocssre  9736  icossre  9737  iccssre  9738  icodisj  9775  iccf1o  9787  fzen  9823  ioom  10038  intfracq  10093  flqdiv  10094  mulqaddmodid  10137  modsumfzodifsn  10169  addmodlteq  10171  remul  10644  sumtp  11183  crth  11900  phimullem  11901  ctiunct  11953  strsetsid  11992  strleund  12047  lmfpm  12412  lmff  12418  lmtopcnp  12419  xmeter  12605  tgqioo  12716  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimolemlt  12802  limcresi  12804  cosordlem  12930