Theorem simp1d 1035

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp1bi  1038  erinxp  6777  exmidapne  7478  addcanprleml  7833  addcanprlemu  7834  ltmprr  7861  lelttrdi  8605  ixxdisj  10137  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccss2  10178  iocssre  10187  icossre  10188  iccssre  10189  icodisj  10226  iccf1o  10238  fzen  10277  ioom  10519  intfracq  10581  flqdiv  10582  mulqaddmodid  10625  modsumfzodifsn  10657  addmodlteq  10659  remul  11432  sumtp  11974  crth  12795  phimullem  12796  eulerthlem1  12798  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  ctiunct  13060  strsetsid  13114  strleund  13185  strext  13187  mhmf  13547  submss  13558  eqger  13810  eqgcpbl  13814  lmodvscl  14318  lssssg  14373  rnglidlmsgrp  14510  2idlcpblrng  14536  lmfpm  14966  lmff  14972  lmtopcnp  14973  xmeter  15159  tgqioo  15278  ivthinclemlopn  15359  ivthinclemuopn  15361  limcimolemlt  15387  limcresi  15389  cosordlem  15572  relogbval  15674  relogbzcl  15675  nnlogbexp  15682  perfectlem2  15723  wlkprop  16177  wlkf  16180  wlkfg  16181  wlkvtxiedg  16195  wlk1walkdom  16209  wlkvtxedg  16213  upgr2wlkdc  16227  isclwwlkng  16256  eupthseg  16302  trlsegvdeglem3  16312  trlsegvdeglem5  16314