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  6888  resixp  7021  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10321  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccgelb  10350  iccss2  10362  icodisj  10410  ioom  10711  elicore  10717  flqdiv  10778  mulqaddmodid  10821  modsumfzodifsn  10853  addmodlteq  10855  immul  11665  sumtp  12205  crth  13030  phimullem  13031  eulerthlem1  13033  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  ballotfilemcdc  13280  ballotfilemfc0  13289  ballotfilemro  13323  ctiunct  13388  structn0fun  13422  strleund  13515  strext  13517  mhmlin  13832  subm0cl  13843  eqger  14085  eqgcpbl  14089  lmodvsdi  14756  lss0cl  14814  rnglidlmsgrp  14942  2idlcpblrng  14968  lmcl  15488  lmtopcnp  15493  xmeter  15679  tgqioo  15798  ivthinclemlopn  15879  ivthinclemuopn  15881  limcimolemlt  15907  limcresi  15909  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  cosordlem  16094  birthdaylem3  16244  perfectlem2  16317  subgruhgredgdm  16733  subumgredg2en  16734  wlkp  16797  wlkpg  16798  wlkvtxiedg  16808  wlk1walkdom  16822  upgr2wlkdc  16840  isclwwlkn  16876  clwwlknwrd  16877  clwwlknon  16892  clwwlknonex2e  16903  trlsegvdeglem3  16925  trlsegvdeglem5  16927  eupth2lem3fi  16939  depindlem2  16970  depindlem3  16971  depind  16972