Theorem simp2d 959

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

Syntax hints:   -> wi 4   /\ w3a 927

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

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

This theorem is referenced by:  simp2bi  962  erinxp  6406  resixp  6530  addcanprleml  7270  addcanprlemu  7271  ltmprr  7298  lelttrdi  8001  ixxdisj  9469  ixxss1  9470  ixxss2  9471  ixxss12  9472  iccgelb  9498  iccss2  9510  icodisj  9558  ioom  9821  flqdiv  9877  mulqaddmodid  9920  modsumfzodifsn  9952  addmodlteq  9954  immul  10444  sumtp  10973  crth  11643  phimullem  11644  structn0fun  11672  strleund  11747  lmcl  12112  lmtopcnp  12117  xmeter  12238  tgqioo  12337