Theorem simp1bi 996

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 993	1 |- ( ph -> ps )

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

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 964

This theorem is referenced by:  limord  4317  smores2  6191  smofvon2dm  6193  smofvon  6196  errel  6438  lincmb01cmp  9786  iccf1o  9787  elfznn0  9894  elfzouz  9928  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  coseq00topi  12916  coseq0negpitopi  12917  cosq34lt1  12931