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  6686  resixp  6810  exmidapne  7354  addcanprleml  7709  addcanprlemu  7710  ltmprr  7737  lelttrdi  8481  ixxdisj  10007  ixxss1  10008  ixxss2  10009  ixxss12  10010  iccsupr  10070  icodisj  10096  ioom  10384  elicore  10390  intfracq  10446  flqdiv  10447  mulqaddmodid  10490  modsumfzodifsn  10522  seqf1oglem2  10646  cjmul  11115  sumtp  11644  crth  12465  eulerthlem1  12468  eulerthlemh  12472  eulerthlemth  12473  4sqlem13m  12645  ennnfonelemim  12714  ctiunct  12730  strsetsid  12784  strleund  12854  strext  12856  mhm0  13218  submcl  13229  submmnd  13230  eqger  13478  eqgcpbl  13482  lmodvsdir  13992  lssclg  14044  rnglidlmsgrp  14177  2idlcpblrng  14203  lmcvg  14607  lmff  14639  lmtopcnp  14640  xmeter  14826  xmetresbl  14830  tgqioo  14945  ivthinclemlopn  15026  ivthinclemuopn  15028  limccl  15049  limcdifap  15052  limcresi  15056  limccnpcntop  15065  limccnp2lem  15066  limccnp2cntop  15067  limccoap  15068  cosordlem  15239  relogbval  15341  relogbzcl  15342  nnlogbexp  15349  mersenne  15387  perfectlem2  15390