Theorem simp2d 1013

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simp2bi  1016  erinxp  6709  resixp  6833  exmidapne  7392  addcanprleml  7747  addcanprlemu  7748  ltmprr  7775  lelttrdi  8519  ixxdisj  10045  ixxss1  10046  ixxss2  10047  ixxss12  10048  iccgelb  10074  iccss2  10086  icodisj  10134  ioom  10425  elicore  10431  flqdiv  10488  mulqaddmodid  10531  modsumfzodifsn  10563  addmodlteq  10565  immul  11265  sumtp  11800  crth  12621  phimullem  12622  eulerthlem1  12624  eulerthlema  12627  eulerthlemh  12628  eulerthlemth  12629  ctiunct  12886  structn0fun  12920  strleund  13010  strext  13012  mhmlin  13374  subm0cl  13385  eqger  13635  eqgcpbl  13639  lmodvsdi  14148  lss0cl  14206  rnglidlmsgrp  14334  2idlcpblrng  14360  lmcl  14792  lmtopcnp  14797  xmeter  14983  tgqioo  15102  ivthinclemlopn  15183  ivthinclemuopn  15185  limcimolemlt  15211  limcresi  15213  limccnpcntop  15222  limccnp2lem  15223  limccnp2cntop  15224  cosordlem  15396  perfectlem2  15547