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  6677  resixp  6801  exmidapne  7345  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  lelttrdi  8472  ixxdisj  9997  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccgelb  10026  iccss2  10038  icodisj  10086  ioom  10369  elicore  10375  flqdiv  10432  mulqaddmodid  10475  modsumfzodifsn  10507  addmodlteq  10509  immul  11063  sumtp  11598  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  ctiunct  12684  structn0fun  12718  strleund  12808  strext  12810  mhmlin  13171  subm0cl  13182  eqger  13432  eqgcpbl  13436  lmodvsdi  13945  lss0cl  14003  rnglidlmsgrp  14131  2idlcpblrng  14157  lmcl  14589  lmtopcnp  14594  xmeter  14780  tgqioo  14899  ivthinclemlopn  14980  ivthinclemuopn  14982  limcimolemlt  15008  limcresi  15010  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  cosordlem  15193  perfectlem2  15344