Theorem simp2d 1010

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

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simp2bi  1013  erinxp  6611  resixp  6735  exmidapne  7261  addcanprleml  7615  addcanprlemu  7616  ltmprr  7643  lelttrdi  8385  ixxdisj  9905  ixxss1  9906  ixxss2  9907  ixxss12  9908  iccgelb  9934  iccss2  9946  icodisj  9994  ioom  10263  elicore  10269  flqdiv  10323  mulqaddmodid  10366  modsumfzodifsn  10398  addmodlteq  10400  immul  10890  sumtp  11424  crth  12226  phimullem  12227  eulerthlem1  12229  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  ctiunct  12443  structn0fun  12477  strleund  12564  strext  12566  mhmlin  12863  subm0cl  12874  eqger  13088  eqgcpbl  13092  lmodvsdi  13406  lss0cl  13460  lmcl  13784  lmtopcnp  13789  xmeter  13975  tgqioo  14086  ivthinclemlopn  14153  ivthinclemuopn  14155  limcimolemlt  14172  limcresi  14174  limccnpcntop  14183  limccnp2lem  14184  limccnp2cntop  14185  cosordlem  14309