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  6843  resixp  6968  exmidapne  7574  addcanprleml  7929  addcanprlemu  7930  ltmprr  7957  lelttrdi  8700  ixxdisj  10236  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccgelb  10265  iccss2  10277  icodisj  10325  ioom  10620  elicore  10626  flqdiv  10683  mulqaddmodid  10726  modsumfzodifsn  10758  addmodlteq  10760  immul  11564  sumtp  12100  crth  12921  phimullem  12922  eulerthlem1  12924  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  ctiunct  13191  structn0fun  13225  strleund  13316  strext  13318  mhmlin  13680  subm0cl  13691  eqger  13941  eqgcpbl  13945  lmodvsdi  14459  lss0cl  14517  rnglidlmsgrp  14645  2idlcpblrng  14671  lmcl  15110  lmtopcnp  15115  xmeter  15301  tgqioo  15420  ivthinclemlopn  15501  ivthinclemuopn  15503  limcimolemlt  15529  limcresi  15531  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  cosordlem  15714  perfectlem2  15868  subgruhgredgdm  16265  subumgredg2en  16266  wlkp  16329  wlkpg  16330  wlkvtxiedg  16340  wlk1walkdom  16354  upgr2wlkdc  16372  isclwwlkn  16408  clwwlknwrd  16409  clwwlknon  16424  clwwlknonex2e  16435  trlsegvdeglem3  16457  trlsegvdeglem5  16459  eupth2lem3fi  16471  depindlem2  16502  depindlem3  16503  depind  16504