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  8754  ixxdisj  10305  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccss2  10346  iocssre  10355  icossre  10356  iccssre  10357  icodisj  10394  iccf1o  10407  fzen  10447  ioom  10695  intfracq  10757  flqdiv  10758  mulqaddmodid  10801  modsumfzodifsn  10833  addmodlteq  10835  remul  11637  sumtp  12181  crth  13002  phimullem  13003  eulerthlem1  13005  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  ballotfilemcdc  13223  ballotfilemfc0  13232  ballotfilemro  13266  ctiunct  13331  strsetsid  13385  strleund  13457  strext  13459  mhmf  13772  submss  13783  eqger  14027  eqgcpbl  14031  lmodvscl  14641  lssssg  14697  rnglidlmsgrp  14834  2idlcpblrng  14860  lmfpm  15344  lmff  15350  lmtopcnp  15351  xmeter  15537  tgqioo  15656  ivthinclemlopn  15737  ivthinclemuopn  15739  limcimolemlt  15765  limcresi  15767  cosordlem  15950  relogbval  16053  relogbzcl  16054  nnlogbexp  16061  perfectlem2  16114  wlkprop  16568  wlkf  16571  wlkfg  16572  wlkvtxiedg  16586  wlk1walkdom  16600  wlkvtxedg  16604  upgr2wlkdc  16618  isclwwlkng  16647  eupthseg  16693  trlsegvdeglem3  16703  trlsegvdeglem5  16705  depindlem2  16748  depindlem3  16749