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  7626  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  lelttrdi  8755  ixxdisj  10315  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccss2  10356  iocssre  10365  icossre  10366  iccssre  10367  icodisj  10404  iccf1o  10417  fzen  10457  ioom  10705  intfracq  10770  flqdiv  10771  mulqaddmodid  10814  modsumfzodifsn  10846  addmodlteq  10848  remul  11651  sumtp  12197  crth  13022  phimullem  13023  eulerthlem1  13025  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  ballotfilemcdc  13272  ballotfilemfc0  13281  ballotfilemro  13315  ctiunct  13380  strsetsid  13434  strleund  13506  strext  13508  mhmf  13821  submss  13832  eqger  14076  eqgcpbl  14080  lmodvscl  14690  lssssg  14746  rnglidlmsgrp  14883  2idlcpblrng  14909  lmfpm  15393  lmff  15399  lmtopcnp  15400  xmeter  15586  tgqioo  15705  ivthinclemlopn  15786  ivthinclemuopn  15788  limcimolemlt  15814  limcresi  15816  cosordlem  16000  relogbval  16106  relogbzcl  16107  nnlogbexp  16114  perfectlem2  16198  wlkprop  16666  wlkf  16669  wlkfg  16670  wlkvtxiedg  16684  wlk1walkdom  16698  wlkvtxedg  16702  upgr2wlkdc  16716  isclwwlkng  16745  eupthseg  16791  trlsegvdeglem3  16801  trlsegvdeglem5  16803  depindlem2  16846  depindlem3  16847