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  6587  addcanprleml  7576  addcanprlemu  7577  ltmprr  7604  lelttrdi  8345  ixxdisj  9860  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccss2  9901  iocssre  9910  icossre  9911  iccssre  9912  icodisj  9949  iccf1o  9961  fzen  9999  ioom  10217  intfracq  10276  flqdiv  10277  mulqaddmodid  10320  modsumfzodifsn  10352  addmodlteq  10354  remul  10836  sumtp  11377  crth  12178  phimullem  12179  eulerthlem1  12181  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  ctiunct  12395  strsetsid  12449  strleund  12506  mhmf  12688  submss  12698  lmfpm  13037  lmff  13043  lmtopcnp  13044  xmeter  13230  tgqioo  13341  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimolemlt  13427  limcresi  13429  cosordlem  13564  relogbval  13663  relogbzcl  13664  nnlogbexp  13671