Theorem simp1d 994

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  simp1bi  997  erinxp  6511  addcanprleml  7446  addcanprlemu  7447  ltmprr  7474  lelttrdi  8212  ixxdisj  9716  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccss2  9757  iocssre  9766  icossre  9767  iccssre  9768  icodisj  9805  iccf1o  9817  fzen  9854  ioom  10069  intfracq  10124  flqdiv  10125  mulqaddmodid  10168  modsumfzodifsn  10200  addmodlteq  10202  remul  10676  sumtp  11215  crth  11936  phimullem  11937  ctiunct  11989  strsetsid  12031  strleund  12086  lmfpm  12451  lmff  12457  lmtopcnp  12458  xmeter  12644  tgqioo  12755  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimolemlt  12841  limcresi  12843  cosordlem  12978  relogbval  13076  relogbzcl  13077  nnlogbexp  13084