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  6887  resixp  7019  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10322  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccsupr  10385  icodisj  10411  ioom  10712  elicore  10718  intfracq  10778  flqdiv  10779  mulqaddmodid  10822  modsumfzodifsn  10854  seqf1oglem2  10978  cjmul  11672  sumtp  12206  crth  13031  eulerthlem1  13034  eulerthlemh  13038  eulerthlemth  13039  4sqlem13m  13211  ballotfilemro  13324  ennnfonelemim  13373  ctiunct  13389  strsetsid  13443  strleund  13516  strext  13518  mhm0  13834  submcl  13845  submmnd  13846  eqger  14086  eqgcpbl  14090  lmodvsdir  14758  lssclg  14810  rnglidlmsgrp  14943  2idlcpblrng  14969  lmcvg  15440  lmff  15472  lmtopcnp  15473  xmeter  15659  xmetresbl  15663  tgqioo  15778  ivthinclemlopn  15859  ivthinclemuopn  15861  limccl  15882  limcdifap  15885  limcresi  15889  limccnpcntop  15898  limccnp2lem  15899  limccnp2cntop  15900  limccoap  15901  cosordlem  16074  relogbval  16184  relogbzcl  16185  nnlogbexp  16192  birthdaylem3  16224  ppiqsval  16237  chtqleppi  16291  mersenne  16294  perfectlem2  16297  subgruhgredgdm  16713  wlk1walkdom  16802  upgr2wlkdc  16820  clwwlknon  16872  clwwlknonex2lem2  16881  depindlem2  16950  depindlem3  16951  depind  16952