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  6608  resixp  6732  exmidapne  7258  addcanprleml  7612  addcanprlemu  7613  ltmprr  7640  lelttrdi  8382  ixxdisj  9902  ixxss1  9903  ixxss2  9904  ixxss12  9905  iccsupr  9965  icodisj  9991  ioom  10260  elicore  10266  intfracq  10319  flqdiv  10320  mulqaddmodid  10363  modsumfzodifsn  10395  cjmul  10893  sumtp  11421  crth  12223  eulerthlem1  12226  eulerthlemh  12230  eulerthlemth  12231  ennnfonelemim  12424  ctiunct  12440  strsetsid  12494  strleund  12561  strext  12563  mhm0  12858  submcl  12869  eqger  13081  eqgcpbl  13085  lmodvsdir  13400  lmcvg  13687  lmff  13719  lmtopcnp  13720  xmeter  13906  xmetresbl  13910  tgqioo  14017  ivthinclemlopn  14084  ivthinclemuopn  14086  limccl  14098  limcdifap  14101  limcresi  14105  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  limccoap  14117  cosordlem  14240  relogbval  14339  relogbzcl  14340  nnlogbexp  14347