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  6612  resixp  6736  exmidapne  7262  addcanprleml  7616  addcanprlemu  7617  ltmprr  7644  lelttrdi  8386  ixxdisj  9906  ixxss1  9907  ixxss2  9908  ixxss12  9909  iccsupr  9969  icodisj  9995  ioom  10264  elicore  10270  intfracq  10323  flqdiv  10324  mulqaddmodid  10367  modsumfzodifsn  10399  cjmul  10897  sumtp  11425  crth  12227  eulerthlem1  12230  eulerthlemh  12234  eulerthlemth  12235  ennnfonelemim  12428  ctiunct  12444  strsetsid  12498  strleund  12565  strext  12567  mhm0  12865  submcl  12876  eqger  13089  eqgcpbl  13093  lmodvsdir  13408  lssclg  13457  lmcvg  13857  lmff  13889  lmtopcnp  13890  xmeter  14076  xmetresbl  14080  tgqioo  14187  ivthinclemlopn  14254  ivthinclemuopn  14256  limccl  14268  limcdifap  14271  limcresi  14275  limccnpcntop  14284  limccnp2lem  14285  limccnp2cntop  14286  limccoap  14287  cosordlem  14410  relogbval  14509  relogbzcl  14510  nnlogbexp  14517