Theorem simp3d 952

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
simp3d	|- ( ph -> th )

Proof of Theorem simp3d

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

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  ax-ia3 106

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

This theorem is referenced by:  simp3bi  955  erinxp  6203  addcanprleml  6804  addcanprlemu  6805  ltmprr  6832  lelttrdi  7530  ixxdisj  8926  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccsupr  8989  icodisj  9014  ioom  9269  intfracq  9322  flqdiv  9323  mulqaddmodid  9366  modsumfzodifsn  9398  cjmul  9772