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  6754  exmidapne  7442  addcanprleml  7797  addcanprlemu  7798  ltmprr  7825  lelttrdi  8569  ixxdisj  10095  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccss2  10136  iocssre  10145  icossre  10146  iccssre  10147  icodisj  10184  iccf1o  10196  fzen  10235  ioom  10475  intfracq  10537  flqdiv  10538  mulqaddmodid  10581  modsumfzodifsn  10613  addmodlteq  10615  remul  11378  sumtp  11920  crth  12741  phimullem  12742  eulerthlem1  12744  eulerthlemfi  12745  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  ctiunct  13006  strsetsid  13060  strleund  13131  strext  13133  mhmf  13493  submss  13504  eqger  13756  eqgcpbl  13760  lmodvscl  14263  lssssg  14318  rnglidlmsgrp  14455  2idlcpblrng  14481  lmfpm  14911  lmff  14917  lmtopcnp  14918  xmeter  15104  tgqioo  15223  ivthinclemlopn  15304  ivthinclemuopn  15306  limcimolemlt  15332  limcresi  15334  cosordlem  15517  relogbval  15619  relogbzcl  15620  nnlogbexp  15627  perfectlem2  15668  wlkfg  16033