Theorem simp2d 1012

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simp2bi  1015  erinxp  6668  resixp  6792  exmidapne  7327  addcanprleml  7681  addcanprlemu  7682  ltmprr  7709  lelttrdi  8453  ixxdisj  9978  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccgelb  10007  iccss2  10019  icodisj  10067  ioom  10350  elicore  10356  flqdiv  10413  mulqaddmodid  10456  modsumfzodifsn  10488  addmodlteq  10490  immul  11044  sumtp  11579  crth  12392  phimullem  12393  eulerthlem1  12395  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  ctiunct  12657  structn0fun  12691  strleund  12781  strext  12783  mhmlin  13099  subm0cl  13110  eqger  13354  eqgcpbl  13358  lmodvsdi  13867  lss0cl  13925  rnglidlmsgrp  14053  2idlcpblrng  14079  lmcl  14481  lmtopcnp  14486  xmeter  14672  tgqioo  14791  ivthinclemlopn  14872  ivthinclemuopn  14874  limcimolemlt  14900  limcresi  14902  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  cosordlem  15085  perfectlem2  15236