Theorem simp3d 1037

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp3bi  1040  erinxp  6778  resixp  6902  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccsupr  10201  icodisj  10227  ioom  10521  elicore  10527  intfracq  10583  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  seqf1oglem2  10783  cjmul  11463  sumtp  11993  crth  12814  eulerthlem1  12817  eulerthlemh  12821  eulerthlemth  12822  4sqlem13m  12994  ennnfonelemim  13063  ctiunct  13079  strsetsid  13133  strleund  13204  strext  13206  mhm0  13569  submcl  13580  submmnd  13581  eqger  13829  eqgcpbl  13833  lmodvsdir  14345  lssclg  14397  rnglidlmsgrp  14530  2idlcpblrng  14556  lmcvg  14960  lmff  14992  lmtopcnp  14993  xmeter  15179  xmetresbl  15183  tgqioo  15298  ivthinclemlopn  15379  ivthinclemuopn  15381  limccl  15402  limcdifap  15405  limcresi  15409  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  limccoap  15421  cosordlem  15592  relogbval  15694  relogbzcl  15695  nnlogbexp  15702  mersenne  15740  perfectlem2  15743  subgruhgredgdm  16140  wlk1walkdom  16229  upgr2wlkdc  16247  clwwlknon  16299  clwwlknonex2lem2  16308  depindlem2  16377  depindlem3  16378  depind  16379