Theorem simp2d 962

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

Syntax hints:   -> wi 4   /\ w3a 930

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 932

This theorem is referenced by:  simp2bi  965  erinxp  6433  resixp  6557  addcanprleml  7323  addcanprlemu  7324  ltmprr  7351  lelttrdi  8055  ixxdisj  9527  ixxss1  9528  ixxss2  9529  ixxss12  9530  iccgelb  9556  iccss2  9568  icodisj  9616  ioom  9879  flqdiv  9935  mulqaddmodid  9978  modsumfzodifsn  10010  addmodlteq  10012  immul  10492  sumtp  11022  crth  11692  phimullem  11693  structn0fun  11754  strleund  11829  lmcl  12195  lmtopcnp  12200  xmeter  12364  tgqioo  12466  limcimolemlt  12513  limcresi  12515  limccnpcntop  12520