Theorem simp1d 999

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  simp1bi  1002  erinxp  6575  addcanprleml  7555  addcanprlemu  7556  ltmprr  7583  lelttrdi  8324  ixxdisj  9839  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccss2  9880  iocssre  9889  icossre  9890  iccssre  9891  icodisj  9928  iccf1o  9940  fzen  9978  ioom  10196  intfracq  10255  flqdiv  10256  mulqaddmodid  10299  modsumfzodifsn  10331  addmodlteq  10333  remul  10814  sumtp  11355  crth  12156  phimullem  12157  eulerthlem1  12159  eulerthlemfi  12160  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  ctiunct  12373  strsetsid  12427  strleund  12483  lmfpm  12883  lmff  12889  lmtopcnp  12890  xmeter  13076  tgqioo  13187  ivthinclemlopn  13254  ivthinclemuopn  13256  limcimolemlt  13273  limcresi  13275  cosordlem  13410  relogbval  13509  relogbzcl  13510  nnlogbexp  13517