Theorem simp1bi 997

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	|- ( ph <-> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
simp1bi	|- ( ph -> ps )

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 119	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 994	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 963

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

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

This theorem is referenced by:  limord  4325  smores2  6199  smofvon2dm  6201  smofvon  6204  errel  6446  lincmb01cmp  9816  iccf1o  9817  elfznn0  9925  elfzouz  9959  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  coseq00topi  12964  coseq0negpitopi  12965  cosq34lt1  12979  cos11  12982