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  6665  resixp  6789  exmidapne  7322  addcanprleml  7676  addcanprlemu  7677  ltmprr  7704  lelttrdi  8447  ixxdisj  9972  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccsupr  10035  icodisj  10061  ioom  10332  elicore  10338  intfracq  10394  flqdiv  10395  mulqaddmodid  10438  modsumfzodifsn  10470  seqf1oglem2  10594  cjmul  11032  sumtp  11560  crth  12365  eulerthlem1  12368  eulerthlemh  12372  eulerthlemth  12373  4sqlem13m  12544  ennnfonelemim  12584  ctiunct  12600  strsetsid  12654  strleund  12724  strext  12726  mhm0  13043  submcl  13054  submmnd  13055  eqger  13297  eqgcpbl  13301  lmodvsdir  13811  lssclg  13863  rnglidlmsgrp  13996  2idlcpblrng  14022  lmcvg  14396  lmff  14428  lmtopcnp  14429  xmeter  14615  xmetresbl  14619  tgqioo  14734  ivthinclemlopn  14815  ivthinclemuopn  14817  limccl  14838  limcdifap  14841  limcresi  14845  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  limccoap  14857  cosordlem  15025  relogbval  15124  relogbzcl  15125  nnlogbexp  15132