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  6888  resixp  7021  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10321  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccsupr  10384  icodisj  10410  ioom  10711  elicore  10717  intfracq  10777  flqdiv  10778  mulqaddmodid  10821  modsumfzodifsn  10853  seqf1oglem2  10977  cjmul  11671  sumtp  12205  crth  13030  eulerthlem1  13033  eulerthlemh  13037  eulerthlemth  13038  4sqlem13m  13210  ballotfilemro  13323  ennnfonelemim  13372  ctiunct  13388  strsetsid  13442  strleund  13515  strext  13517  mhm0  13833  submcl  13844  submmnd  13845  eqger  14085  eqgcpbl  14089  lmodvsdir  14757  lssclg  14809  rnglidlmsgrp  14942  2idlcpblrng  14968  lmcvg  15460  lmff  15492  lmtopcnp  15493  xmeter  15679  xmetresbl  15683  tgqioo  15798  ivthinclemlopn  15879  ivthinclemuopn  15881  limccl  15902  limcdifap  15905  limcresi  15909  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  limccoap  15921  cosordlem  16094  relogbval  16204  relogbzcl  16205  nnlogbexp  16212  birthdaylem3  16244  ppiqsval  16257  chtqleppi  16311  mersenne  16314  perfectlem2  16317  subgruhgredgdm  16733  wlk1walkdom  16822  upgr2wlkdc  16840  clwwlknon  16892  clwwlknonex2lem2  16901  depindlem2  16970  depindlem3  16971  depind  16972