Theorem simp2d 951

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
simp2d	|- ( ph -> ch )

Proof of Theorem simp2d

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

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simp2bi  954  erinxp  6203  addcanprleml  6804  addcanprlemu  6805  ltmprr  6832  lelttrdi  7530  ixxdisj  8926  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccgelb  8955  iccss2  8967  icodisj  9014  ioom  9269  flqdiv  9323  mulqaddmodid  9366  modsumfzodifsn  9398  addmodlteq  9400  immul  9766