Theorem simp3d 978

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

Syntax hints:   -> wi 4   /\ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simp3bi  981  erinxp  6457  resixp  6581  addcanprleml  7370  addcanprlemu  7371  ltmprr  7398  lelttrdi  8107  ixxdisj  9579  ixxss1  9580  ixxss2  9581  ixxss12  9582  iccsupr  9642  icodisj  9668  ioom  9931  intfracq  9986  flqdiv  9987  mulqaddmodid  10030  modsumfzodifsn  10062  cjmul  10550  sumtp  11075  crth  11745  ennnfonelemim  11782  ctiunct  11796  strsetsid  11835  strleund  11890  lmcvg  12228  lmff  12260  lmtopcnp  12261  xmeter  12425  xmetresbl  12429  tgqioo  12533  limccl  12584  limcdifap  12587  limcresi  12591  limccnpcntop  12600  limccnp2lem  12601  limccnp2cntop  12602