Theorem simp3d 1006

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

Syntax hints:   -> wi 4   /\ w3a 973

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

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

This theorem is referenced by:  simp3bi  1009  erinxp  6587  resixp  6711  addcanprleml  7576  addcanprlemu  7577  ltmprr  7604  lelttrdi  8345  ixxdisj  9860  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccsupr  9923  icodisj  9949  ioom  10217  elicore  10223  intfracq  10276  flqdiv  10277  mulqaddmodid  10320  modsumfzodifsn  10352  cjmul  10849  sumtp  11377  crth  12178  eulerthlem1  12181  eulerthlemh  12185  eulerthlemth  12186  ennnfonelemim  12379  ctiunct  12395  strsetsid  12449  strleund  12506  mhm0  12691  submcl  12701  lmcvg  13011  lmff  13043  lmtopcnp  13044  xmeter  13230  xmetresbl  13234  tgqioo  13341  ivthinclemlopn  13408  ivthinclemuopn  13410  limccl  13422  limcdifap  13425  limcresi  13429  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  limccoap  13441  cosordlem  13564  relogbval  13663  relogbzcl  13664  nnlogbexp  13671