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 )

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

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

This theorem is referenced by:  simp2bi  1044  erinxp  6873  resixp  7005  exmidapne  7616  addcanprleml  7971  addcanprlemu  7972  ltmprr  7999  lelttrdi  8744  ixxdisj  10284  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccgelb  10313  iccss2  10325  icodisj  10373  ioom  10673  elicore  10679  flqdiv  10736  mulqaddmodid  10779  modsumfzodifsn  10811  addmodlteq  10813  immul  11622  sumtp  12159  crth  12980  phimullem  12981  eulerthlem1  12983  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  ballotfilemcdc  13201  ballotfilemfc0  13210  ballotfilemro  13244  ctiunct  13309  structn0fun  13343  strleund  13434  strext  13436  mhmlin  13751  subm0cl  13762  eqger  14004  eqgcpbl  14008  lmodvsdi  14620  lss0cl  14678  rnglidlmsgrp  14806  2idlcpblrng  14832  lmcl  15269  lmtopcnp  15274  xmeter  15460  tgqioo  15579  ivthinclemlopn  15660  ivthinclemuopn  15662  limcimolemlt  15688  limcresi  15690  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  cosordlem  15873  perfectlem2  16028  subgruhgredgdm  16425  subumgredg2en  16426  wlkp  16489  wlkpg  16490  wlkvtxiedg  16500  wlk1walkdom  16514  upgr2wlkdc  16532  isclwwlkn  16568  clwwlknwrd  16569  clwwlknon  16584  clwwlknonex2e  16595  trlsegvdeglem3  16617  trlsegvdeglem5  16619  eupth2lem3fi  16631  depindlem2  16662  depindlem3  16663  depind  16664