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  6665  resixp  6789  exmidapne  7322  addcanprleml  7676  addcanprlemu  7677  ltmprr  7704  lelttrdi  8447  ixxdisj  9972  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccgelb  10001  iccss2  10013  icodisj  10061  ioom  10332  elicore  10338  flqdiv  10395  mulqaddmodid  10438  modsumfzodifsn  10470  addmodlteq  10472  immul  11026  sumtp  11560  crth  12365  phimullem  12366  eulerthlem1  12368  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  ctiunct  12600  structn0fun  12634  strleund  12724  strext  12726  mhmlin  13042  subm0cl  13053  eqger  13297  eqgcpbl  13301  lmodvsdi  13810  lss0cl  13868  rnglidlmsgrp  13996  2idlcpblrng  14022  lmcl  14424  lmtopcnp  14429  xmeter  14615  tgqioo  14734  ivthinclemlopn  14815  ivthinclemuopn  14817  limcimolemlt  14843  limcresi  14845  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  cosordlem  15025