Theorem simp2d 1034

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp2bi  1037  erinxp  6773  resixp  6897  exmidapne  7469  addcanprleml  7824  addcanprlemu  7825  ltmprr  7852  lelttrdi  8596  ixxdisj  10128  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccgelb  10157  iccss2  10169  icodisj  10217  ioom  10510  elicore  10516  flqdiv  10573  mulqaddmodid  10616  modsumfzodifsn  10648  addmodlteq  10650  immul  11430  sumtp  11965  crth  12786  phimullem  12787  eulerthlem1  12789  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  ctiunct  13051  structn0fun  13085  strleund  13176  strext  13178  mhmlin  13540  subm0cl  13551  eqger  13801  eqgcpbl  13805  lmodvsdi  14315  lss0cl  14373  rnglidlmsgrp  14501  2idlcpblrng  14527  lmcl  14959  lmtopcnp  14964  xmeter  15150  tgqioo  15269  ivthinclemlopn  15350  ivthinclemuopn  15352  limcimolemlt  15378  limcresi  15380  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  cosordlem  15563  perfectlem2  15714  wlkp  16131  wlkpg  16132  wlkvtxiedg  16142  wlk1walkdom  16156  upgr2wlkdc  16172  isclwwlkn  16208  clwwlknwrd  16209  clwwlknon  16224  clwwlknonex2e  16235