Theorem simp2d 1041

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp2bi  1044  erinxp  6883  resixp  7015  exmidapne  7627  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  lelttrdi  8756  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccgelb  10345  iccss2  10357  icodisj  10405  ioom  10706  elicore  10712  flqdiv  10773  mulqaddmodid  10816  modsumfzodifsn  10848  addmodlteq  10850  immul  11660  sumtp  12200  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  ballotfilemcdc  13275  ballotfilemfc0  13284  ballotfilemro  13318  ctiunct  13383  structn0fun  13417  strleund  13510  strext  13512  mhmlin  13827  subm0cl  13838  eqger  14080  eqgcpbl  14084  lmodvsdi  14732  lss0cl  14790  rnglidlmsgrp  14918  2idlcpblrng  14944  lmcl  15437  lmtopcnp  15442  xmeter  15628  tgqioo  15747  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limcresi  15858  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  cosordlem  16042  birthdaylem3  16188  perfectlem2  16261  subgruhgredgdm  16677  subumgredg2en  16678  wlkp  16741  wlkpg  16742  wlkvtxiedg  16752  wlk1walkdom  16766  upgr2wlkdc  16784  isclwwlkn  16820  clwwlknwrd  16821  clwwlknon  16836  clwwlknonex2e  16847  trlsegvdeglem3  16869  trlsegvdeglem5  16871  eupth2lem3fi  16883  depindlem2  16914  depindlem3  16915  depind  16916