Theorem simp2d 1000

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 988	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simp2bi  1003  erinxp  6575  resixp  6699  addcanprleml  7555  addcanprlemu  7556  ltmprr  7583  lelttrdi  8324  ixxdisj  9839  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccgelb  9868  iccss2  9880  icodisj  9928  ioom  10196  elicore  10202  flqdiv  10256  mulqaddmodid  10299  modsumfzodifsn  10331  addmodlteq  10333  immul  10821  sumtp  11355  crth  12156  phimullem  12157  eulerthlem1  12159  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  ctiunct  12373  structn0fun  12407  strleund  12483  lmcl  12885  lmtopcnp  12890  xmeter  13076  tgqioo  13187  ivthinclemlopn  13254  ivthinclemuopn  13256  limcimolemlt  13273  limcresi  13275  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  cosordlem  13410