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  15443  lmff  15475  lmtopcnp  15476  xmeter  15662  xmetresbl  15666  tgqioo  15781  ivthinclemlopn  15862  ivthinclemuopn  15864  limccl  15885  limcdifap  15888  limcresi  15892  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  limccoap  15904  cosordlem  16077  relogbval  16187  relogbzcl  16188  nnlogbexp  16195  birthdaylem3  16227  ppiqsval  16240  chtqleppi  16294  mersenne  16297  perfectlem2  16300  subgruhgredgdm  16716  wlk1walkdom  16805  upgr2wlkdc  16823  clwwlknon  16875  clwwlknonex2lem2  16884  depindlem2  16953  depindlem3  16954  depind  16955