Theorem simp3d 1013

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

Syntax hints:   -> wi 4   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simp3bi  1016  erinxp  6668  resixp  6792  exmidapne  7327  addcanprleml  7681  addcanprlemu  7682  ltmprr  7709  lelttrdi  8453  ixxdisj  9978  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccsupr  10041  icodisj  10067  ioom  10350  elicore  10356  intfracq  10412  flqdiv  10413  mulqaddmodid  10456  modsumfzodifsn  10488  seqf1oglem2  10612  cjmul  11050  sumtp  11579  crth  12392  eulerthlem1  12395  eulerthlemh  12399  eulerthlemth  12400  4sqlem13m  12572  ennnfonelemim  12641  ctiunct  12657  strsetsid  12711  strleund  12781  strext  12783  mhm0  13100  submcl  13111  submmnd  13112  eqger  13354  eqgcpbl  13358  lmodvsdir  13868  lssclg  13920  rnglidlmsgrp  14053  2idlcpblrng  14079  lmcvg  14453  lmff  14485  lmtopcnp  14486  xmeter  14672  xmetresbl  14676  tgqioo  14791  ivthinclemlopn  14872  ivthinclemuopn  14874  limccl  14895  limcdifap  14898  limcresi  14902  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  limccoap  14914  cosordlem  15085  relogbval  15187  relogbzcl  15188  nnlogbexp  15195  mersenne  15233  perfectlem2  15236