Theorem simp1d 1040

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
simp1d	|- ( ph -> ps )

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp1 1028	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ w3a 1009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

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

This theorem is referenced by:  simp1bi  1043  erinxp  6873  exmidapne  7616  addcanprleml  7971  addcanprlemu  7972  ltmprr  7999  lelttrdi  8744  ixxdisj  10284  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccss2  10325  iocssre  10334  icossre  10335  iccssre  10336  icodisj  10373  iccf1o  10386  fzen  10426  ioom  10673  intfracq  10735  flqdiv  10736  mulqaddmodid  10779  modsumfzodifsn  10811  addmodlteq  10813  remul  11615  sumtp  12159  crth  12980  phimullem  12981  eulerthlem1  12983  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  ballotfilemcdc  13201  ballotfilemfc0  13210  ballotfilemro  13244  ctiunct  13309  strsetsid  13363  strleund  13434  strext  13436  mhmf  13749  submss  13760  eqger  14004  eqgcpbl  14008  lmodvscl  14614  lssssg  14669  rnglidlmsgrp  14806  2idlcpblrng  14832  lmfpm  15267  lmff  15273  lmtopcnp  15274  xmeter  15460  tgqioo  15579  ivthinclemlopn  15660  ivthinclemuopn  15662  limcimolemlt  15688  limcresi  15690  cosordlem  15873  relogbval  15976  relogbzcl  15977  nnlogbexp  15984  perfectlem2  16028  wlkprop  16482  wlkf  16485  wlkfg  16486  wlkvtxiedg  16500  wlk1walkdom  16514  wlkvtxedg  16518  upgr2wlkdc  16532  isclwwlkng  16561  eupthseg  16607  trlsegvdeglem3  16617  trlsegvdeglem5  16619  depindlem2  16662  depindlem3  16663