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  6888  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10321  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccss2  10362  iocssre  10371  icossre  10372  iccssre  10373  icodisj  10410  iccf1o  10423  fzen  10463  ioom  10711  intfracq  10777  flqdiv  10778  mulqaddmodid  10821  modsumfzodifsn  10853  addmodlteq  10855  remul  11658  sumtp  12205  crth  13030  phimullem  13031  eulerthlem1  13033  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  ballotfilemcdc  13280  ballotfilemfc0  13289  ballotfilemro  13323  ctiunct  13388  strsetsid  13442  strleund  13515  strext  13517  mhmf  13830  submss  13841  eqger  14085  eqgcpbl  14089  lmodvscl  14749  lssssg  14805  rnglidlmsgrp  14942  2idlcpblrng  14968  lmfpm  15486  lmff  15492  lmtopcnp  15493  xmeter  15679  tgqioo  15798  ivthinclemlopn  15879  ivthinclemuopn  15881  limcimolemlt  15907  limcresi  15909  cosordlem  16094  relogbval  16204  relogbzcl  16205  nnlogbexp  16212  perfectlem2  16317  wlkprop  16790  wlkf  16793  wlkfg  16794  wlkvtxiedg  16808  wlk1walkdom  16822  wlkvtxedg  16826  upgr2wlkdc  16840  isclwwlkng  16869  eupthseg  16915  trlsegvdeglem3  16925  trlsegvdeglem5  16927  depindlem2  16970  depindlem3  16971