Theorem simp1d 1036

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 1024	. 2 |- ( ( ps /\ ch /\ th ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simp1bi  1039  erinxp  6856  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8717  ixxdisj  10255  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  iocssre  10305  icossre  10306  iccssre  10307  icodisj  10344  iccf1o  10357  fzen  10397  ioom  10644  intfracq  10706  flqdiv  10707  mulqaddmodid  10750  modsumfzodifsn  10782  addmodlteq  10784  remul  11582  sumtp  12125  crth  12946  phimullem  12947  eulerthlem1  12949  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  ballotfilemcdc  13167  ballotfilemfc0  13176  ballotfilemro  13210  ctiunct  13275  strsetsid  13329  strleund  13400  strext  13402  mhmf  13720  submss  13731  eqger  13977  eqgcpbl  13981  lmodvscl  14579  lssssg  14634  rnglidlmsgrp  14771  2idlcpblrng  14797  lmfpm  15234  lmff  15240  lmtopcnp  15241  xmeter  15427  tgqioo  15546  ivthinclemlopn  15627  ivthinclemuopn  15629  limcimolemlt  15655  limcresi  15657  cosordlem  15840  relogbval  15942  relogbzcl  15943  nnlogbexp  15950  perfectlem2  15994  wlkprop  16448  wlkf  16451  wlkfg  16452  wlkvtxiedg  16466  wlk1walkdom  16480  wlkvtxedg  16484  upgr2wlkdc  16498  isclwwlkng  16527  eupthseg  16573  trlsegvdeglem3  16583  trlsegvdeglem5  16585  depindlem2  16628  depindlem3  16629