Theorem simp1d 1033

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp1bi  1036  erinxp  6773  exmidapne  7469  addcanprleml  7824  addcanprlemu  7825  ltmprr  7852  lelttrdi  8596  ixxdisj  10128  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccss2  10169  iocssre  10178  icossre  10179  iccssre  10180  icodisj  10217  iccf1o  10229  fzen  10268  ioom  10510  intfracq  10572  flqdiv  10573  mulqaddmodid  10616  modsumfzodifsn  10648  addmodlteq  10650  remul  11423  sumtp  11965  crth  12786  phimullem  12787  eulerthlem1  12789  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  ctiunct  13051  strsetsid  13105  strleund  13176  strext  13178  mhmf  13538  submss  13549  eqger  13801  eqgcpbl  13805  lmodvscl  14309  lssssg  14364  rnglidlmsgrp  14501  2idlcpblrng  14527  lmfpm  14957  lmff  14963  lmtopcnp  14964  xmeter  15150  tgqioo  15269  ivthinclemlopn  15350  ivthinclemuopn  15352  limcimolemlt  15378  limcresi  15380  cosordlem  15563  relogbval  15665  relogbzcl  15666  nnlogbexp  15673  perfectlem2  15714  wlkprop  16124  wlkf  16127  wlkfg  16128  wlkvtxiedg  16142  wlk1walkdom  16156  wlkvtxedg  16160  upgr2wlkdc  16172  isclwwlkng  16201  eupthseg  16247