Theorem simp1d 1036

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp1bi  1039  erinxp  6843  exmidapne  7574  addcanprleml  7929  addcanprlemu  7930  ltmprr  7957  lelttrdi  8700  ixxdisj  10236  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccss2  10277  iocssre  10286  icossre  10287  iccssre  10288  icodisj  10325  iccf1o  10338  fzen  10377  ioom  10620  intfracq  10682  flqdiv  10683  mulqaddmodid  10726  modsumfzodifsn  10758  addmodlteq  10760  remul  11557  sumtp  12100  crth  12921  phimullem  12922  eulerthlem1  12924  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  ctiunct  13191  strsetsid  13245  strleund  13316  strext  13318  mhmf  13678  submss  13689  eqger  13941  eqgcpbl  13945  lmodvscl  14453  lssssg  14508  rnglidlmsgrp  14645  2idlcpblrng  14671  lmfpm  15108  lmff  15114  lmtopcnp  15115  xmeter  15301  tgqioo  15420  ivthinclemlopn  15501  ivthinclemuopn  15503  limcimolemlt  15529  limcresi  15531  cosordlem  15714  relogbval  15816  relogbzcl  15817  nnlogbexp  15824  perfectlem2  15868  wlkprop  16322  wlkf  16325  wlkfg  16326  wlkvtxiedg  16340  wlk1walkdom  16354  wlkvtxedg  16358  upgr2wlkdc  16372  isclwwlkng  16401  eupthseg  16447  trlsegvdeglem3  16457  trlsegvdeglem5  16459  depindlem2  16502  depindlem3  16503