Theorem simp3d 1038

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp3bi  1041  erinxp  6821  resixp  6945  exmidapne  7522  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  lelttrdi  8648  ixxdisj  10182  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccsupr  10245  icodisj  10271  ioom  10566  elicore  10572  intfracq  10628  flqdiv  10629  mulqaddmodid  10672  modsumfzodifsn  10704  seqf1oglem2  10828  cjmul  11508  sumtp  12038  crth  12859  eulerthlem1  12862  eulerthlemh  12866  eulerthlemth  12867  4sqlem13m  13039  ennnfonelemim  13108  ctiunct  13124  strsetsid  13178  strleund  13249  strext  13251  mhm0  13614  submcl  13625  submmnd  13626  eqger  13874  eqgcpbl  13878  lmodvsdir  14391  lssclg  14443  rnglidlmsgrp  14576  2idlcpblrng  14602  lmcvg  15011  lmff  15043  lmtopcnp  15044  xmeter  15230  xmetresbl  15234  tgqioo  15349  ivthinclemlopn  15430  ivthinclemuopn  15432  limccl  15453  limcdifap  15456  limcresi  15460  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  limccoap  15472  cosordlem  15643  relogbval  15745  relogbzcl  15746  nnlogbexp  15753  mersenne  15794  perfectlem2  15797  subgruhgredgdm  16194  wlk1walkdom  16283  upgr2wlkdc  16301  clwwlknon  16353  clwwlknonex2lem2  16362  depindlem2  16431  depindlem3  16432  depind  16433