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  6695  resixp  6819  exmidapne  7371  addcanprleml  7726  addcanprlemu  7727  ltmprr  7754  lelttrdi  8498  ixxdisj  10024  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccsupr  10087  icodisj  10113  ioom  10401  elicore  10407  intfracq  10463  flqdiv  10464  mulqaddmodid  10507  modsumfzodifsn  10539  seqf1oglem2  10663  cjmul  11138  sumtp  11667  crth  12488  eulerthlem1  12491  eulerthlemh  12495  eulerthlemth  12496  4sqlem13m  12668  ennnfonelemim  12737  ctiunct  12753  strsetsid  12807  strleund  12877  strext  12879  mhm0  13242  submcl  13253  submmnd  13254  eqger  13502  eqgcpbl  13506  lmodvsdir  14016  lssclg  14068  rnglidlmsgrp  14201  2idlcpblrng  14227  lmcvg  14631  lmff  14663  lmtopcnp  14664  xmeter  14850  xmetresbl  14854  tgqioo  14969  ivthinclemlopn  15050  ivthinclemuopn  15052  limccl  15073  limcdifap  15076  limcresi  15080  limccnpcntop  15089  limccnp2lem  15090  limccnp2cntop  15091  limccoap  15092  cosordlem  15263  relogbval  15365  relogbzcl  15366  nnlogbexp  15373  mersenne  15411  perfectlem2  15414