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  6599  resixp  6723  addcanprleml  7588  addcanprlemu  7589  ltmprr  7616  lelttrdi  8357  ixxdisj  9874  ixxss1  9875  ixxss2  9876  ixxss12  9877  iccgelb  9903  iccss2  9915  icodisj  9963  ioom  10231  elicore  10237  flqdiv  10291  mulqaddmodid  10334  modsumfzodifsn  10366  addmodlteq  10368  immul  10856  sumtp  11390  crth  12191  phimullem  12192  eulerthlem1  12194  eulerthlema  12197  eulerthlemh  12198  eulerthlemth  12199  ctiunct  12408  structn0fun  12442  strleund  12528  mhmlin  12730  subm0cl  12740  lmcl  13325  lmtopcnp  13330  xmeter  13516  tgqioo  13627  ivthinclemlopn  13694  ivthinclemuopn  13696  limcimolemlt  13713  limcresi  13715  limccnpcntop  13724  limccnp2lem  13725  limccnp2cntop  13726  cosordlem  13850