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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  simp3bi  1045  erinxp  6873  resixp  7005  exmidapne  7616  addcanprleml  7971  addcanprlemu  7972  ltmprr  7999  lelttrdi  8744  ixxdisj  10284  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccsupr  10347  icodisj  10373  ioom  10673  elicore  10679  intfracq  10735  flqdiv  10736  mulqaddmodid  10779  modsumfzodifsn  10811  seqf1oglem2  10935  cjmul  11628  sumtp  12159  crth  12980  eulerthlem1  12983  eulerthlemh  12987  eulerthlemth  12988  4sqlem13m  13160  ballotfilemro  13244  ennnfonelemim  13293  ctiunct  13309  strsetsid  13363  strleund  13434  strext  13436  mhm0  13752  submcl  13763  submmnd  13764  eqger  14004  eqgcpbl  14008  lmodvsdir  14621  lssclg  14673  rnglidlmsgrp  14806  2idlcpblrng  14832  lmcvg  15241  lmff  15273  lmtopcnp  15274  xmeter  15460  xmetresbl  15464  tgqioo  15579  ivthinclemlopn  15660  ivthinclemuopn  15662  limccl  15683  limcdifap  15686  limcresi  15690  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  limccoap  15702  cosordlem  15873  relogbval  15976  relogbzcl  15977  nnlogbexp  15984  mersenne  16025  perfectlem2  16028  subgruhgredgdm  16425  wlk1walkdom  16514  upgr2wlkdc  16532  clwwlknon  16584  clwwlknonex2lem2  16593  depindlem2  16662  depindlem3  16663  depind  16664