Theorem simp1d 1010

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

Syntax hints:   -> wi 4   /\ w3a 979

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 981

This theorem is referenced by:  simp1bi  1013  erinxp  6622  exmidapne  7272  addcanprleml  7626  addcanprlemu  7627  ltmprr  7654  lelttrdi  8396  ixxdisj  9916  ixxss1  9917  ixxss2  9918  ixxss12  9919  iccss2  9957  iocssre  9966  icossre  9967  iccssre  9968  icodisj  10005  iccf1o  10017  fzen  10056  ioom  10274  intfracq  10333  flqdiv  10334  mulqaddmodid  10377  modsumfzodifsn  10409  addmodlteq  10411  remul  10894  sumtp  11435  crth  12237  phimullem  12238  eulerthlem1  12240  eulerthlemfi  12241  eulerthlemrprm  12242  eulerthlema  12243  eulerthlemh  12244  eulerthlemth  12245  ctiunct  12454  strsetsid  12508  strleund  12576  strext  12578  mhmf  12877  submss  12888  eqger  13115  eqgcpbl  13119  lmodvscl  13489  lssssg  13544  lmfpm  14014  lmff  14020  lmtopcnp  14021  xmeter  14207  tgqioo  14318  ivthinclemlopn  14385  ivthinclemuopn  14387  limcimolemlt  14404  limcresi  14406  cosordlem  14541  relogbval  14640  relogbzcl  14641  nnlogbexp  14648