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 )

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

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

This theorem is used by:  simp1bi  1043  erinxp  6883  exmidapne  7627  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  lelttrdi  8756  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iocssre  10366  icossre  10367  iccssre  10368  icodisj  10405  iccf1o  10418  fzen  10458  ioom  10706  intfracq  10772  flqdiv  10773  mulqaddmodid  10816  modsumfzodifsn  10848  addmodlteq  10850  remul  11653  sumtp  12200  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  ballotfilemcdc  13275  ballotfilemfc0  13284  ballotfilemro  13318  ctiunct  13383  strsetsid  13437  strleund  13510  strext  13512  mhmf  13825  submss  13836  eqger  14080  eqgcpbl  14084  lmodvscl  14725  lssssg  14781  rnglidlmsgrp  14918  2idlcpblrng  14944  lmfpm  15435  lmff  15441  lmtopcnp  15442  xmeter  15628  tgqioo  15747  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limcresi  15858  cosordlem  16042  relogbval  16148  relogbzcl  16149  nnlogbexp  16156  perfectlem2  16261  wlkprop  16734  wlkf  16737  wlkfg  16738  wlkvtxiedg  16752  wlk1walkdom  16766  wlkvtxedg  16770  upgr2wlkdc  16784  isclwwlkng  16813  eupthseg  16859  trlsegvdeglem3  16869  trlsegvdeglem5  16871  depindlem2  16914  depindlem3  16915