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  6821  resixp  6945  exmidapne  7522  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  lelttrdi  8648  ixxdisj  10182  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccgelb  10211  iccss2  10223  icodisj  10271  ioom  10566  elicore  10572  flqdiv  10629  mulqaddmodid  10672  modsumfzodifsn  10704  addmodlteq  10706  immul  11502  sumtp  12038  crth  12859  phimullem  12860  eulerthlem1  12862  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  ctiunct  13124  structn0fun  13158  strleund  13249  strext  13251  mhmlin  13613  subm0cl  13624  eqger  13874  eqgcpbl  13878  lmodvsdi  14390  lss0cl  14448  rnglidlmsgrp  14576  2idlcpblrng  14602  lmcl  15039  lmtopcnp  15044  xmeter  15230  tgqioo  15349  ivthinclemlopn  15430  ivthinclemuopn  15432  limcimolemlt  15458  limcresi  15460  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  cosordlem  15643  perfectlem2  15797  subgruhgredgdm  16194  subumgredg2en  16195  wlkp  16258  wlkpg  16259  wlkvtxiedg  16269  wlk1walkdom  16283  upgr2wlkdc  16301  isclwwlkn  16337  clwwlknwrd  16338  clwwlknon  16353  clwwlknonex2e  16364  trlsegvdeglem3  16386  trlsegvdeglem5  16388  eupth2lem3fi  16400  depindlem2  16431  depindlem3  16432  depind  16433