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  7343  addcanprleml  7698  addcanprlemu  7699  ltmprr  7726  lelttrdi  8470  ixxdisj  9995  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccsupr  10058  icodisj  10084  ioom  10367  elicore  10373  intfracq  10429  flqdiv  10430  mulqaddmodid  10473  modsumfzodifsn  10505  seqf1oglem2  10629  cjmul  11067  sumtp  11596  crth  12417  eulerthlem1  12420  eulerthlemh  12424  eulerthlemth  12425  4sqlem13m  12597  ennnfonelemim  12666  ctiunct  12682  strsetsid  12736  strleund  12806  strext  12808  mhm0  13170  submcl  13181  submmnd  13182  eqger  13430  eqgcpbl  13434  lmodvsdir  13944  lssclg  13996  rnglidlmsgrp  14129  2idlcpblrng  14155  lmcvg  14537  lmff  14569  lmtopcnp  14570  xmeter  14756  xmetresbl  14760  tgqioo  14875  ivthinclemlopn  14956  ivthinclemuopn  14958  limccl  14979  limcdifap  14982  limcresi  14986  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  limccoap  14998  cosordlem  15169  relogbval  15271  relogbzcl  15272  nnlogbexp  15279  mersenne  15317  perfectlem2  15320