Theorem simp1d 1036

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp1bi  1039  erinxp  6821  exmidapne  7522  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  lelttrdi  8648  ixxdisj  10182  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccss2  10223  iocssre  10232  icossre  10233  iccssre  10234  icodisj  10271  iccf1o  10284  fzen  10323  ioom  10566  intfracq  10628  flqdiv  10629  mulqaddmodid  10672  modsumfzodifsn  10704  addmodlteq  10706  remul  11495  sumtp  12038  crth  12859  phimullem  12860  eulerthlem1  12862  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  ctiunct  13124  strsetsid  13178  strleund  13249  strext  13251  mhmf  13611  submss  13622  eqger  13874  eqgcpbl  13878  lmodvscl  14384  lssssg  14439  rnglidlmsgrp  14576  2idlcpblrng  14602  lmfpm  15037  lmff  15043  lmtopcnp  15044  xmeter  15230  tgqioo  15349  ivthinclemlopn  15430  ivthinclemuopn  15432  limcimolemlt  15458  limcresi  15460  cosordlem  15643  relogbval  15745  relogbzcl  15746  nnlogbexp  15753  perfectlem2  15797  wlkprop  16251  wlkf  16254  wlkfg  16255  wlkvtxiedg  16269  wlk1walkdom  16283  wlkvtxedg  16287  upgr2wlkdc  16301  isclwwlkng  16330  eupthseg  16376  trlsegvdeglem3  16386  trlsegvdeglem5  16388  depindlem2  16431  depindlem3  16432