Theorem simp3d 1042

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp3bi  1045  erinxp  6883  resixp  7015  exmidapne  7627  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  lelttrdi  8756  ixxdisj  10316  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccsupr  10379  icodisj  10405  ioom  10706  elicore  10712  intfracq  10772  flqdiv  10773  mulqaddmodid  10816  modsumfzodifsn  10848  seqf1oglem2  10972  cjmul  11666  sumtp  12200  crth  13025  eulerthlem1  13028  eulerthlemh  13032  eulerthlemth  13033  4sqlem13m  13205  ballotfilemro  13318  ennnfonelemim  13367  ctiunct  13383  strsetsid  13437  strleund  13510  strext  13512  mhm0  13828  submcl  13839  submmnd  13840  eqger  14080  eqgcpbl  14084  lmodvsdir  14733  lssclg  14785  rnglidlmsgrp  14918  2idlcpblrng  14944  lmcvg  15409  lmff  15441  lmtopcnp  15442  xmeter  15628  xmetresbl  15632  tgqioo  15747  ivthinclemlopn  15828  ivthinclemuopn  15830  limccl  15851  limcdifap  15854  limcresi  15858  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  limccoap  15870  cosordlem  16042  relogbval  16148  relogbzcl  16149  nnlogbexp  16156  birthdaylem3  16188  ppiqsval  16201  chtqleppi  16255  mersenne  16258  perfectlem2  16261  subgruhgredgdm  16677  wlk1walkdom  16766  upgr2wlkdc  16784  clwwlknon  16836  clwwlknonex2lem2  16845  depindlem2  16914  depindlem3  16915  depind  16916