Theorem simp3d 1014

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp3bi  1017  erinxp  6709  resixp  6833  exmidapne  7392  addcanprleml  7747  addcanprlemu  7748  ltmprr  7775  lelttrdi  8519  ixxdisj  10045  ixxss1  10046  ixxss2  10047  ixxss12  10048  iccsupr  10108  icodisj  10134  ioom  10425  elicore  10431  intfracq  10487  flqdiv  10488  mulqaddmodid  10531  modsumfzodifsn  10563  seqf1oglem2  10687  cjmul  11271  sumtp  11800  crth  12621  eulerthlem1  12624  eulerthlemh  12628  eulerthlemth  12629  4sqlem13m  12801  ennnfonelemim  12870  ctiunct  12886  strsetsid  12940  strleund  13010  strext  13012  mhm0  13375  submcl  13386  submmnd  13387  eqger  13635  eqgcpbl  13639  lmodvsdir  14149  lssclg  14201  rnglidlmsgrp  14334  2idlcpblrng  14360  lmcvg  14764  lmff  14796  lmtopcnp  14797  xmeter  14983  xmetresbl  14987  tgqioo  15102  ivthinclemlopn  15183  ivthinclemuopn  15185  limccl  15206  limcdifap  15209  limcresi  15213  limccnpcntop  15222  limccnp2lem  15223  limccnp2cntop  15224  limccoap  15225  cosordlem  15396  relogbval  15498  relogbzcl  15499  nnlogbexp  15506  mersenne  15544  perfectlem2  15547