Theorem simp2d 1036

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
simp2d	|- ( ph -> ch )

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
2		simp2 1024	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ w3a 1004

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

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

This theorem is referenced by:  simp2bi  1039  erinxp  6777  resixp  6901  exmidapne  7478  addcanprleml  7833  addcanprlemu  7834  ltmprr  7861  lelttrdi  8605  ixxdisj  10137  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccgelb  10166  iccss2  10178  icodisj  10226  ioom  10519  elicore  10525  flqdiv  10582  mulqaddmodid  10625  modsumfzodifsn  10657  addmodlteq  10659  immul  11439  sumtp  11974  crth  12795  phimullem  12796  eulerthlem1  12798  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  ctiunct  13060  structn0fun  13094  strleund  13185  strext  13187  mhmlin  13549  subm0cl  13560  eqger  13810  eqgcpbl  13814  lmodvsdi  14324  lss0cl  14382  rnglidlmsgrp  14510  2idlcpblrng  14536  lmcl  14968  lmtopcnp  14973  xmeter  15159  tgqioo  15278  ivthinclemlopn  15359  ivthinclemuopn  15361  limcimolemlt  15387  limcresi  15389  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  cosordlem  15572  perfectlem2  15723  subgruhgredgdm  16120  subumgredg2en  16121  wlkp  16184  wlkpg  16185  wlkvtxiedg  16195  wlk1walkdom  16209  upgr2wlkdc  16227  isclwwlkn  16263  clwwlknwrd  16264  clwwlknon  16279  clwwlknonex2e  16290  trlsegvdeglem3  16312  trlsegvdeglem5  16314