Theorem simp3d 1035

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp3bi  1038  erinxp  6764  resixp  6888  exmidapne  7457  addcanprleml  7812  addcanprlemu  7813  ltmprr  7840  lelttrdi  8584  ixxdisj  10111  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccsupr  10174  icodisj  10200  ioom  10492  elicore  10498  intfracq  10554  flqdiv  10555  mulqaddmodid  10598  modsumfzodifsn  10630  seqf1oglem2  10754  cjmul  11411  sumtp  11940  crth  12761  eulerthlem1  12764  eulerthlemh  12768  eulerthlemth  12769  4sqlem13m  12941  ennnfonelemim  13010  ctiunct  13026  strsetsid  13080  strleund  13151  strext  13153  mhm0  13516  submcl  13527  submmnd  13528  eqger  13776  eqgcpbl  13780  lmodvsdir  14291  lssclg  14343  rnglidlmsgrp  14476  2idlcpblrng  14502  lmcvg  14906  lmff  14938  lmtopcnp  14939  xmeter  15125  xmetresbl  15129  tgqioo  15244  ivthinclemlopn  15325  ivthinclemuopn  15327  limccl  15348  limcdifap  15351  limcresi  15355  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  limccoap  15367  cosordlem  15538  relogbval  15640  relogbzcl  15641  nnlogbexp  15648  mersenne  15686  perfectlem2  15689  wlk1walkdom  16100  upgr2wlkdc  16116