Theorem simp1d 1011

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

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simp1bi  1014  erinxp  6663  exmidapne  7320  addcanprleml  7674  addcanprlemu  7675  ltmprr  7702  lelttrdi  8445  ixxdisj  9969  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccss2  10010  iocssre  10019  icossre  10020  iccssre  10021  icodisj  10058  iccf1o  10070  fzen  10109  ioom  10329  intfracq  10391  flqdiv  10392  mulqaddmodid  10435  modsumfzodifsn  10467  addmodlteq  10469  remul  11016  sumtp  11557  crth  12362  phimullem  12363  eulerthlem1  12365  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  ctiunct  12597  strsetsid  12651  strleund  12721  strext  12723  mhmf  13037  submss  13048  eqger  13294  eqgcpbl  13298  lmodvscl  13801  lssssg  13856  rnglidlmsgrp  13993  2idlcpblrng  14019  lmfpm  14411  lmff  14417  lmtopcnp  14418  xmeter  14604  tgqioo  14715  ivthinclemlopn  14790  ivthinclemuopn  14792  limcimolemlt  14818  limcresi  14820  cosordlem  14984  relogbval  15083  relogbzcl  15084  nnlogbexp  15091