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  6754  resixp  6878  exmidapne  7442  addcanprleml  7797  addcanprlemu  7798  ltmprr  7825  lelttrdi  8569  ixxdisj  10095  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccgelb  10124  iccss2  10136  icodisj  10184  ioom  10475  elicore  10481  flqdiv  10538  mulqaddmodid  10581  modsumfzodifsn  10613  addmodlteq  10615  immul  11385  sumtp  11920  crth  12741  phimullem  12742  eulerthlem1  12744  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  ctiunct  13006  structn0fun  13040  strleund  13131  strext  13133  mhmlin  13495  subm0cl  13506  eqger  13756  eqgcpbl  13760  lmodvsdi  14269  lss0cl  14327  rnglidlmsgrp  14455  2idlcpblrng  14481  lmcl  14913  lmtopcnp  14918  xmeter  15104  tgqioo  15223  ivthinclemlopn  15304  ivthinclemuopn  15306  limcimolemlt  15332  limcresi  15334  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  cosordlem  15517  perfectlem2  15668  wlkpg  16035