Theorem simp3d 1011

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
simp3d	|- ( ph -> th )

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp3 999	. 2 |- ( ( ps /\ ch /\ th ) -> th )
3	1, 2	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simp3bi  1014  erinxp  6609  resixp  6733  exmidapne  7259  addcanprleml  7613  addcanprlemu  7614  ltmprr  7641  lelttrdi  8383  ixxdisj  9903  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccsupr  9966  icodisj  9992  ioom  10261  elicore  10267  intfracq  10320  flqdiv  10321  mulqaddmodid  10364  modsumfzodifsn  10396  cjmul  10894  sumtp  11422  crth  12224  eulerthlem1  12227  eulerthlemh  12231  eulerthlemth  12232  ennnfonelemim  12425  ctiunct  12441  strsetsid  12495  strleund  12562  strext  12564  mhm0  12859  submcl  12870  eqger  13083  eqgcpbl  13087  lmodvsdir  13402  lmcvg  13720  lmff  13752  lmtopcnp  13753  xmeter  13939  xmetresbl  13943  tgqioo  14050  ivthinclemlopn  14117  ivthinclemuopn  14119  limccl  14131  limcdifap  14134  limcresi  14138  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  limccoap  14150  cosordlem  14273  relogbval  14372  relogbzcl  14373  nnlogbexp  14380