Theorem simp1d 1012

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp1bi  1015  erinxp  6696  exmidapne  7372  addcanprleml  7727  addcanprlemu  7728  ltmprr  7755  lelttrdi  8499  ixxdisj  10025  ixxss1  10026  ixxss2  10027  ixxss12  10028  iccss2  10066  iocssre  10075  icossre  10076  iccssre  10077  icodisj  10114  iccf1o  10126  fzen  10165  ioom  10403  intfracq  10465  flqdiv  10466  mulqaddmodid  10509  modsumfzodifsn  10541  addmodlteq  10543  remul  11183  sumtp  11725  crth  12546  phimullem  12547  eulerthlem1  12549  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  ctiunct  12811  strsetsid  12865  strleund  12935  strext  12937  mhmf  13297  submss  13308  eqger  13560  eqgcpbl  13564  lmodvscl  14067  lssssg  14122  rnglidlmsgrp  14259  2idlcpblrng  14285  lmfpm  14715  lmff  14721  lmtopcnp  14722  xmeter  14908  tgqioo  15027  ivthinclemlopn  15108  ivthinclemuopn  15110  limcimolemlt  15136  limcresi  15138  cosordlem  15321  relogbval  15423  relogbzcl  15424  nnlogbexp  15431  perfectlem2  15472