Theorem simp3d 1001

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

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simp3bi  1004  erinxp  6575  resixp  6699  addcanprleml  7555  addcanprlemu  7556  ltmprr  7583  lelttrdi  8324  ixxdisj  9839  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccsupr  9902  icodisj  9928  ioom  10196  elicore  10202  intfracq  10255  flqdiv  10256  mulqaddmodid  10299  modsumfzodifsn  10331  cjmul  10827  sumtp  11355  crth  12156  eulerthlem1  12159  eulerthlemh  12163  eulerthlemth  12164  ennnfonelemim  12357  ctiunct  12373  strsetsid  12427  strleund  12483  lmcvg  12867  lmff  12899  lmtopcnp  12900  xmeter  13086  xmetresbl  13090  tgqioo  13197  ivthinclemlopn  13264  ivthinclemuopn  13266  limccl  13278  limcdifap  13281  limcresi  13285  limccnpcntop  13294  limccnp2lem  13295  limccnp2cntop  13296  limccoap  13297  cosordlem  13420  relogbval  13519  relogbzcl  13520  nnlogbexp  13527