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  6663  resixp  6787  exmidapne  7320  addcanprleml  7674  addcanprlemu  7675  ltmprr  7702  lelttrdi  8445  ixxdisj  9969  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccgelb  9998  iccss2  10010  icodisj  10058  ioom  10329  elicore  10335  flqdiv  10392  mulqaddmodid  10435  modsumfzodifsn  10467  addmodlteq  10469  immul  11023  sumtp  11557  crth  12362  phimullem  12363  eulerthlem1  12365  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  ctiunct  12597  structn0fun  12631  strleund  12721  strext  12723  mhmlin  13039  subm0cl  13050  eqger  13294  eqgcpbl  13298  lmodvsdi  13807  lss0cl  13865  rnglidlmsgrp  13993  2idlcpblrng  14019  lmcl  14413  lmtopcnp  14418  xmeter  14604  tgqioo  14715  ivthinclemlopn  14790  ivthinclemuopn  14792  limcimolemlt  14818  limcresi  14820  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  cosordlem  14984