Theorem simp1d 1035

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp1bi  1038  erinxp  6778  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iocssre  10188  icossre  10189  iccssre  10190  icodisj  10227  iccf1o  10239  fzen  10278  ioom  10521  intfracq  10583  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  addmodlteq  10661  remul  11450  sumtp  11993  crth  12814  phimullem  12815  eulerthlem1  12817  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  ctiunct  13079  strsetsid  13133  strleund  13204  strext  13206  mhmf  13566  submss  13577  eqger  13829  eqgcpbl  13833  lmodvscl  14338  lssssg  14393  rnglidlmsgrp  14530  2idlcpblrng  14556  lmfpm  14986  lmff  14992  lmtopcnp  14993  xmeter  15179  tgqioo  15298  ivthinclemlopn  15379  ivthinclemuopn  15381  limcimolemlt  15407  limcresi  15409  cosordlem  15592  relogbval  15694  relogbzcl  15695  nnlogbexp  15702  perfectlem2  15743  wlkprop  16197  wlkf  16200  wlkfg  16201  wlkvtxiedg  16215  wlk1walkdom  16229  wlkvtxedg  16233  upgr2wlkdc  16247  isclwwlkng  16276  eupthseg  16322  trlsegvdeglem3  16332  trlsegvdeglem5  16334  depindlem2  16377  depindlem3  16378