Theorem simp2d 1005

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
simp2d	|- ( ph -> ch )

Proof of Theorem simp2d

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

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

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

This theorem is referenced by:  simp2bi  1008  erinxp  6587  resixp  6711  addcanprleml  7576  addcanprlemu  7577  ltmprr  7604  lelttrdi  8345  ixxdisj  9860  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccgelb  9889  iccss2  9901  icodisj  9949  ioom  10217  elicore  10223  flqdiv  10277  mulqaddmodid  10320  modsumfzodifsn  10352  addmodlteq  10354  immul  10843  sumtp  11377  crth  12178  phimullem  12179  eulerthlem1  12181  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  ctiunct  12395  structn0fun  12429  strleund  12506  mhmlin  12690  subm0cl  12700  lmcl  13039  lmtopcnp  13044  xmeter  13230  tgqioo  13341  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimolemlt  13427  limcresi  13429  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  cosordlem  13564