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  6695  resixp  6819  exmidapne  7371  addcanprleml  7726  addcanprlemu  7727  ltmprr  7754  lelttrdi  8498  ixxdisj  10024  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccgelb  10053  iccss2  10065  icodisj  10113  ioom  10401  elicore  10407  flqdiv  10464  mulqaddmodid  10507  modsumfzodifsn  10539  addmodlteq  10541  immul  11132  sumtp  11667  crth  12488  phimullem  12489  eulerthlem1  12491  eulerthlema  12494  eulerthlemh  12495  eulerthlemth  12496  ctiunct  12753  structn0fun  12787  strleund  12877  strext  12879  mhmlin  13241  subm0cl  13252  eqger  13502  eqgcpbl  13506  lmodvsdi  14015  lss0cl  14073  rnglidlmsgrp  14201  2idlcpblrng  14227  lmcl  14659  lmtopcnp  14664  xmeter  14850  tgqioo  14969  ivthinclemlopn  15050  ivthinclemuopn  15052  limcimolemlt  15078  limcresi  15080  limccnpcntop  15089  limccnp2lem  15090  limccnp2cntop  15091  cosordlem  15263  perfectlem2  15414