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  6764  exmidapne  7457  addcanprleml  7812  addcanprlemu  7813  ltmprr  7840  lelttrdi  8584  ixxdisj  10111  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccss2  10152  iocssre  10161  icossre  10162  iccssre  10163  icodisj  10200  iccf1o  10212  fzen  10251  ioom  10492  intfracq  10554  flqdiv  10555  mulqaddmodid  10598  modsumfzodifsn  10630  addmodlteq  10632  remul  11398  sumtp  11940  crth  12761  phimullem  12762  eulerthlem1  12764  eulerthlemfi  12765  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  ctiunct  13026  strsetsid  13080  strleund  13151  strext  13153  mhmf  13513  submss  13524  eqger  13776  eqgcpbl  13780  lmodvscl  14284  lssssg  14339  rnglidlmsgrp  14476  2idlcpblrng  14502  lmfpm  14932  lmff  14938  lmtopcnp  14939  xmeter  15125  tgqioo  15244  ivthinclemlopn  15325  ivthinclemuopn  15327  limcimolemlt  15353  limcresi  15355  cosordlem  15538  relogbval  15640  relogbzcl  15641  nnlogbexp  15648  perfectlem2  15689  wlkprop  16068  wlkf  16071  wlkfg  16072  wlkvtxiedg  16086  wlk1walkdom  16100  wlkvtxedg  16104  upgr2wlkdc  16116