Theorem simp1d 1012

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp1bi  1015  erinxp  6714  exmidapne  7402  addcanprleml  7757  addcanprlemu  7758  ltmprr  7785  lelttrdi  8529  ixxdisj  10055  ixxss1  10056  ixxss2  10057  ixxss12  10058  iccss2  10096  iocssre  10105  icossre  10106  iccssre  10107  icodisj  10144  iccf1o  10156  fzen  10195  ioom  10435  intfracq  10497  flqdiv  10498  mulqaddmodid  10541  modsumfzodifsn  10573  addmodlteq  10575  remul  11268  sumtp  11810  crth  12631  phimullem  12632  eulerthlem1  12634  eulerthlemfi  12635  eulerthlemrprm  12636  eulerthlema  12637  eulerthlemh  12638  eulerthlemth  12639  ctiunct  12896  strsetsid  12950  strleund  13020  strext  13022  mhmf  13382  submss  13393  eqger  13645  eqgcpbl  13649  lmodvscl  14152  lssssg  14207  rnglidlmsgrp  14344  2idlcpblrng  14370  lmfpm  14800  lmff  14806  lmtopcnp  14807  xmeter  14993  tgqioo  15112  ivthinclemlopn  15193  ivthinclemuopn  15195  limcimolemlt  15221  limcresi  15223  cosordlem  15406  relogbval  15508  relogbzcl  15509  nnlogbexp  15516  perfectlem2  15557