Theorem simp2d 1037

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

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

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

This theorem is referenced by:  simp2bi  1040  erinxp  6856  resixp  6981  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8717  ixxdisj  10255  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccgelb  10284  iccss2  10296  icodisj  10344  ioom  10644  elicore  10650  flqdiv  10707  mulqaddmodid  10750  modsumfzodifsn  10782  addmodlteq  10784  immul  11589  sumtp  12125  crth  12946  phimullem  12947  eulerthlem1  12949  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  ballotfilemcdc  13167  ballotfilemfc0  13176  ballotfilemro  13210  ctiunct  13275  structn0fun  13309  strleund  13400  strext  13402  mhmlin  13722  subm0cl  13733  eqger  13977  eqgcpbl  13981  lmodvsdi  14585  lss0cl  14643  rnglidlmsgrp  14771  2idlcpblrng  14797  lmcl  15236  lmtopcnp  15241  xmeter  15427  tgqioo  15546  ivthinclemlopn  15627  ivthinclemuopn  15629  limcimolemlt  15655  limcresi  15657  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  cosordlem  15840  perfectlem2  15994  subgruhgredgdm  16391  subumgredg2en  16392  wlkp  16455  wlkpg  16456  wlkvtxiedg  16466  wlk1walkdom  16480  upgr2wlkdc  16498  isclwwlkn  16534  clwwlknwrd  16535  clwwlknon  16550  clwwlknonex2e  16561  trlsegvdeglem3  16583  trlsegvdeglem5  16585  eupth2lem3fi  16597  depindlem2  16628  depindlem3  16629  depind  16630