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  6677  resixp  6801  exmidapne  7345  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  lelttrdi  8472  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccsupr  10060  icodisj  10086  ioom  10369  elicore  10375  intfracq  10431  flqdiv  10432  mulqaddmodid  10475  modsumfzodifsn  10507  seqf1oglem2  10631  cjmul  11069  sumtp  11598  crth  12419  eulerthlem1  12422  eulerthlemh  12426  eulerthlemth  12427  4sqlem13m  12599  ennnfonelemim  12668  ctiunct  12684  strsetsid  12738  strleund  12808  strext  12810  mhm0  13172  submcl  13183  submmnd  13184  eqger  13432  eqgcpbl  13436  lmodvsdir  13946  lssclg  13998  rnglidlmsgrp  14131  2idlcpblrng  14157  lmcvg  14561  lmff  14593  lmtopcnp  14594  xmeter  14780  xmetresbl  14784  tgqioo  14899  ivthinclemlopn  14980  ivthinclemuopn  14982  limccl  15003  limcdifap  15006  limcresi  15010  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  limccoap  15022  cosordlem  15193  relogbval  15295  relogbzcl  15296  nnlogbexp  15303  mersenne  15341  perfectlem2  15344