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  6887  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10322  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccss2  10363  iocssre  10372  icossre  10373  iccssre  10374  icodisj  10411  iccf1o  10424  fzen  10464  ioom  10712  intfracq  10778  flqdiv  10779  mulqaddmodid  10822  modsumfzodifsn  10854  addmodlteq  10856  remul  11659  sumtp  12206  crth  13031  phimullem  13032  eulerthlem1  13034  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  ballotfilemcdc  13281  ballotfilemfc0  13290  ballotfilemro  13324  ctiunct  13389  strsetsid  13443  strleund  13516  strext  13518  mhmf  13831  submss  13842  eqger  14086  eqgcpbl  14090  lmodvscl  14750  lssssg  14806  rnglidlmsgrp  14943  2idlcpblrng  14969  lmfpm  15469  lmff  15475  lmtopcnp  15476  xmeter  15662  tgqioo  15781  ivthinclemlopn  15862  ivthinclemuopn  15864  limcimolemlt  15890  limcresi  15892  cosordlem  16077  relogbval  16187  relogbzcl  16188  nnlogbexp  16195  perfectlem2  16300  wlkprop  16773  wlkf  16776  wlkfg  16777  wlkvtxiedg  16791  wlk1walkdom  16805  wlkvtxedg  16809  upgr2wlkdc  16823  isclwwlkng  16852  eupthseg  16898  trlsegvdeglem3  16908  trlsegvdeglem5  16910  depindlem2  16953  depindlem3  16954