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  11437  sumtp  11980  crth  12801  phimullem  12802  eulerthlem1  12804  eulerthlemfi  12805  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  ctiunct  13066  strsetsid  13120  strleund  13191  strext  13193  mhmf  13553  submss  13564  eqger  13816  eqgcpbl  13820  lmodvscl  14325  lssssg  14380  rnglidlmsgrp  14517  2idlcpblrng  14543  lmfpm  14973  lmff  14979  lmtopcnp  14980  xmeter  15166  tgqioo  15285  ivthinclemlopn  15366  ivthinclemuopn  15368  limcimolemlt  15394  limcresi  15396  cosordlem  15579  relogbval  15681  relogbzcl  15682  nnlogbexp  15689  perfectlem2  15730  wlkprop  16184  wlkf  16187  wlkfg  16188  wlkvtxiedg  16202  wlk1walkdom  16216  wlkvtxedg  16220  upgr2wlkdc  16234  isclwwlkng  16263  eupthseg  16309  trlsegvdeglem3  16319  trlsegvdeglem5  16321  depindlem2  16352  depindlem3  16353