Theorem simp3d 1035

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp3bi  1038  erinxp  6773  resixp  6897  exmidapne  7469  addcanprleml  7824  addcanprlemu  7825  ltmprr  7852  lelttrdi  8596  ixxdisj  10128  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccsupr  10191  icodisj  10217  ioom  10510  elicore  10516  intfracq  10572  flqdiv  10573  mulqaddmodid  10616  modsumfzodifsn  10648  seqf1oglem2  10772  cjmul  11436  sumtp  11965  crth  12786  eulerthlem1  12789  eulerthlemh  12793  eulerthlemth  12794  4sqlem13m  12966  ennnfonelemim  13035  ctiunct  13051  strsetsid  13105  strleund  13176  strext  13178  mhm0  13541  submcl  13552  submmnd  13553  eqger  13801  eqgcpbl  13805  lmodvsdir  14316  lssclg  14368  rnglidlmsgrp  14501  2idlcpblrng  14527  lmcvg  14931  lmff  14963  lmtopcnp  14964  xmeter  15150  xmetresbl  15154  tgqioo  15269  ivthinclemlopn  15350  ivthinclemuopn  15352  limccl  15373  limcdifap  15376  limcresi  15380  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  limccoap  15392  cosordlem  15563  relogbval  15665  relogbzcl  15666  nnlogbexp  15673  mersenne  15711  perfectlem2  15714  wlk1walkdom  16156  upgr2wlkdc  16172  clwwlknon  16224  clwwlknonex2lem2  16233