Theorem simp2d 1036

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp2bi  1039  erinxp  6778  resixp  6902  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccgelb  10167  iccss2  10179  icodisj  10227  ioom  10521  elicore  10527  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  addmodlteq  10661  immul  11457  sumtp  11993  crth  12814  phimullem  12815  eulerthlem1  12817  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  ctiunct  13079  structn0fun  13113  strleund  13204  strext  13206  mhmlin  13568  subm0cl  13579  eqger  13829  eqgcpbl  13833  lmodvsdi  14344  lss0cl  14402  rnglidlmsgrp  14530  2idlcpblrng  14556  lmcl  14988  lmtopcnp  14993  xmeter  15179  tgqioo  15298  ivthinclemlopn  15379  ivthinclemuopn  15381  limcimolemlt  15407  limcresi  15409  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  cosordlem  15592  perfectlem2  15743  subgruhgredgdm  16140  subumgredg2en  16141  wlkp  16204  wlkpg  16205  wlkvtxiedg  16215  wlk1walkdom  16229  upgr2wlkdc  16247  isclwwlkn  16283  clwwlknwrd  16284  clwwlknon  16299  clwwlknonex2e  16310  trlsegvdeglem3  16332  trlsegvdeglem5  16334  eupth2lem3fi  16346  depindlem2  16377  depindlem3  16378  depind  16379