Theorem simp1d 1004

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  simp1bi  1007  erinxp  6583  addcanprleml  7563  addcanprlemu  7564  ltmprr  7591  lelttrdi  8332  ixxdisj  9847  ixxss1  9848  ixxss2  9849  ixxss12  9850  iccss2  9888  iocssre  9897  icossre  9898  iccssre  9899  icodisj  9936  iccf1o  9948  fzen  9986  ioom  10204  intfracq  10263  flqdiv  10264  mulqaddmodid  10307  modsumfzodifsn  10339  addmodlteq  10341  remul  10823  sumtp  11364  crth  12165  phimullem  12166  eulerthlem1  12168  eulerthlemfi  12169  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  ctiunct  12382  strsetsid  12436  strleund  12493  mhmf  12675  submss  12685  lmfpm  12996  lmff  13002  lmtopcnp  13003  xmeter  13189  tgqioo  13300  ivthinclemlopn  13367  ivthinclemuopn  13369  limcimolemlt  13386  limcresi  13388  cosordlem  13523  relogbval  13622  relogbzcl  13623  nnlogbexp  13630