Theorem simp2d 1041

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp2bi  1044  erinxp  6887  resixp  7019  exmidapne  7632  addcanprleml  7987  addcanprlemu  7988  ltmprr  8015  lelttrdi  8761  ixxdisj  10322  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccgelb  10351  iccss2  10363  icodisj  10411  ioom  10712  elicore  10718  flqdiv  10779  mulqaddmodid  10822  modsumfzodifsn  10854  addmodlteq  10856  immul  11666  sumtp  12206  crth  13031  phimullem  13032  eulerthlem1  13034  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  ballotfilemcdc  13281  ballotfilemfc0  13290  ballotfilemro  13324  ctiunct  13389  structn0fun  13423  strleund  13516  strext  13518  mhmlin  13833  subm0cl  13844  eqger  14086  eqgcpbl  14090  lmodvsdi  14757  lss0cl  14815  rnglidlmsgrp  14943  2idlcpblrng  14969  lmcl  15471  lmtopcnp  15476  xmeter  15662  tgqioo  15781  ivthinclemlopn  15862  ivthinclemuopn  15864  limcimolemlt  15890  limcresi  15892  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  cosordlem  16077  birthdaylem3  16227  perfectlem2  16300  subgruhgredgdm  16716  subumgredg2en  16717  wlkp  16780  wlkpg  16781  wlkvtxiedg  16791  wlk1walkdom  16805  upgr2wlkdc  16823  isclwwlkn  16859  clwwlknwrd  16860  clwwlknon  16875  clwwlknonex2e  16886  trlsegvdeglem3  16908  trlsegvdeglem5  16910  eupth2lem3fi  16922  depindlem2  16953  depindlem3  16954  depind  16955