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  6777  resixp  6901  exmidapne  7478  addcanprleml  7833  addcanprlemu  7834  ltmprr  7861  lelttrdi  8605  ixxdisj  10137  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccsupr  10200  icodisj  10226  ioom  10519  elicore  10525  intfracq  10581  flqdiv  10582  mulqaddmodid  10625  modsumfzodifsn  10657  seqf1oglem2  10781  cjmul  11445  sumtp  11974  crth  12795  eulerthlem1  12798  eulerthlemh  12802  eulerthlemth  12803  4sqlem13m  12975  ennnfonelemim  13044  ctiunct  13060  strsetsid  13114  strleund  13185  strext  13187  mhm0  13550  submcl  13561  submmnd  13562  eqger  13810  eqgcpbl  13814  lmodvsdir  14325  lssclg  14377  rnglidlmsgrp  14510  2idlcpblrng  14536  lmcvg  14940  lmff  14972  lmtopcnp  14973  xmeter  15159  xmetresbl  15163  tgqioo  15278  ivthinclemlopn  15359  ivthinclemuopn  15361  limccl  15382  limcdifap  15385  limcresi  15389  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  limccoap  15401  cosordlem  15572  relogbval  15674  relogbzcl  15675  nnlogbexp  15682  mersenne  15720  perfectlem2  15723  subgruhgredgdm  16120  wlk1walkdom  16209  upgr2wlkdc  16227  clwwlknon  16279  clwwlknonex2lem2  16288