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  6764  resixp  6888  exmidapne  7457  addcanprleml  7812  addcanprlemu  7813  ltmprr  7840  lelttrdi  8584  ixxdisj  10111  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccgelb  10140  iccss2  10152  icodisj  10200  ioom  10492  elicore  10498  flqdiv  10555  mulqaddmodid  10598  modsumfzodifsn  10630  addmodlteq  10632  immul  11405  sumtp  11940  crth  12761  phimullem  12762  eulerthlem1  12764  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  ctiunct  13026  structn0fun  13060  strleund  13151  strext  13153  mhmlin  13515  subm0cl  13526  eqger  13776  eqgcpbl  13780  lmodvsdi  14290  lss0cl  14348  rnglidlmsgrp  14476  2idlcpblrng  14502  lmcl  14934  lmtopcnp  14939  xmeter  15125  tgqioo  15244  ivthinclemlopn  15325  ivthinclemuopn  15327  limcimolemlt  15353  limcresi  15355  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  cosordlem  15538  perfectlem2  15689  wlkp  16075  wlkpg  16076  wlkvtxiedg  16086  wlk1walkdom  16100  upgr2wlkdc  16116