Theorem simp3d 1038

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp3bi  1041  erinxp  6843  resixp  6968  exmidapne  7574  addcanprleml  7929  addcanprlemu  7930  ltmprr  7957  lelttrdi  8700  ixxdisj  10236  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccsupr  10299  icodisj  10325  ioom  10620  elicore  10626  intfracq  10682  flqdiv  10683  mulqaddmodid  10726  modsumfzodifsn  10758  seqf1oglem2  10882  cjmul  11570  sumtp  12100  crth  12921  eulerthlem1  12924  eulerthlemh  12928  eulerthlemth  12929  4sqlem13m  13101  ennnfonelemim  13175  ctiunct  13191  strsetsid  13245  strleund  13316  strext  13318  mhm0  13681  submcl  13692  submmnd  13693  eqger  13941  eqgcpbl  13945  lmodvsdir  14460  lssclg  14512  rnglidlmsgrp  14645  2idlcpblrng  14671  lmcvg  15082  lmff  15114  lmtopcnp  15115  xmeter  15301  xmetresbl  15305  tgqioo  15420  ivthinclemlopn  15501  ivthinclemuopn  15503  limccl  15524  limcdifap  15527  limcresi  15531  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  limccoap  15543  cosordlem  15714  relogbval  15816  relogbzcl  15817  nnlogbexp  15824  mersenne  15865  perfectlem2  15868  subgruhgredgdm  16265  wlk1walkdom  16354  upgr2wlkdc  16372  clwwlknon  16424  clwwlknonex2lem2  16433  depindlem2  16502  depindlem3  16503  depind  16504