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  6686  resixp  6810  exmidapne  7354  addcanprleml  7709  addcanprlemu  7710  ltmprr  7737  lelttrdi  8481  ixxdisj  10007  ixxss1  10008  ixxss2  10009  ixxss12  10010  iccgelb  10036  iccss2  10048  icodisj  10096  ioom  10384  elicore  10390  flqdiv  10447  mulqaddmodid  10490  modsumfzodifsn  10522  addmodlteq  10524  immul  11109  sumtp  11644  crth  12465  phimullem  12466  eulerthlem1  12468  eulerthlema  12471  eulerthlemh  12472  eulerthlemth  12473  ctiunct  12730  structn0fun  12764  strleund  12854  strext  12856  mhmlin  13217  subm0cl  13228  eqger  13478  eqgcpbl  13482  lmodvsdi  13991  lss0cl  14049  rnglidlmsgrp  14177  2idlcpblrng  14203  lmcl  14635  lmtopcnp  14640  xmeter  14826  tgqioo  14945  ivthinclemlopn  15026  ivthinclemuopn  15028  limcimolemlt  15054  limcresi  15056  limccnpcntop  15065  limccnp2lem  15066  limccnp2cntop  15067  cosordlem  15239  perfectlem2  15390