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  6754  resixp  6878  exmidapne  7442  addcanprleml  7797  addcanprlemu  7798  ltmprr  7825  lelttrdi  8569  ixxdisj  10095  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccsupr  10158  icodisj  10184  ioom  10475  elicore  10481  intfracq  10537  flqdiv  10538  mulqaddmodid  10581  modsumfzodifsn  10613  seqf1oglem2  10737  cjmul  11391  sumtp  11920  crth  12741  eulerthlem1  12744  eulerthlemh  12748  eulerthlemth  12749  4sqlem13m  12921  ennnfonelemim  12990  ctiunct  13006  strsetsid  13060  strleund  13131  strext  13133  mhm0  13496  submcl  13507  submmnd  13508  eqger  13756  eqgcpbl  13760  lmodvsdir  14270  lssclg  14322  rnglidlmsgrp  14455  2idlcpblrng  14481  lmcvg  14885  lmff  14917  lmtopcnp  14918  xmeter  15104  xmetresbl  15108  tgqioo  15223  ivthinclemlopn  15304  ivthinclemuopn  15306  limccl  15327  limcdifap  15330  limcresi  15334  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  limccoap  15346  cosordlem  15517  relogbval  15619  relogbzcl  15620  nnlogbexp  15627  mersenne  15665  perfectlem2  15668