Theorem simp3d 1013

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
simp3d	|- ( ph -> th )

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp3 1001	. 2 |- ( ( ps /\ ch /\ th ) -> th )
3	1, 2	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 980

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

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

This theorem is referenced by:  simp3bi  1016  erinxp  6663  resixp  6787  exmidapne  7320  addcanprleml  7674  addcanprlemu  7675  ltmprr  7702  lelttrdi  8445  ixxdisj  9969  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccsupr  10032  icodisj  10058  ioom  10329  elicore  10335  intfracq  10391  flqdiv  10392  mulqaddmodid  10435  modsumfzodifsn  10467  seqf1oglem2  10591  cjmul  11029  sumtp  11557  crth  12362  eulerthlem1  12365  eulerthlemh  12369  eulerthlemth  12370  4sqlem13m  12541  ennnfonelemim  12581  ctiunct  12597  strsetsid  12651  strleund  12721  strext  12723  mhm0  13040  submcl  13051  submmnd  13052  eqger  13294  eqgcpbl  13298  lmodvsdir  13808  lssclg  13860  rnglidlmsgrp  13993  2idlcpblrng  14019  lmcvg  14385  lmff  14417  lmtopcnp  14418  xmeter  14604  xmetresbl  14608  tgqioo  14715  ivthinclemlopn  14790  ivthinclemuopn  14792  limccl  14813  limcdifap  14816  limcresi  14820  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  limccoap  14832  cosordlem  14984  relogbval  15083  relogbzcl  15084  nnlogbexp  15091