Theorem simp1d 1011

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simp1bi  1014  erinxp  6695  exmidapne  7371  addcanprleml  7726  addcanprlemu  7727  ltmprr  7754  lelttrdi  8498  ixxdisj  10024  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccss2  10065  iocssre  10074  icossre  10075  iccssre  10076  icodisj  10113  iccf1o  10125  fzen  10164  ioom  10401  intfracq  10463  flqdiv  10464  mulqaddmodid  10507  modsumfzodifsn  10539  addmodlteq  10541  remul  11154  sumtp  11696  crth  12517  phimullem  12518  eulerthlem1  12520  eulerthlemfi  12521  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  ctiunct  12782  strsetsid  12836  strleund  12906  strext  12908  mhmf  13268  submss  13279  eqger  13531  eqgcpbl  13535  lmodvscl  14038  lssssg  14093  rnglidlmsgrp  14230  2idlcpblrng  14256  lmfpm  14686  lmff  14692  lmtopcnp  14693  xmeter  14879  tgqioo  14998  ivthinclemlopn  15079  ivthinclemuopn  15081  limcimolemlt  15107  limcresi  15109  cosordlem  15292  relogbval  15394  relogbzcl  15395  nnlogbexp  15402  perfectlem2  15443