Theorem simp1bi 1002

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

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

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 970

This theorem is referenced by:  limord  4372  smores2  6258  smofvon2dm  6260  smofvon  6263  errel  6506  lincmb01cmp  9935  iccf1o  9936  elfznn0  10045  elfzouz  10082  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  eulerthlema  12158  modprm0  12182  gzcn  12298  coseq00topi  13356  coseq0negpitopi  13357  cosq34lt1  13371  cos11  13374  nconstwlpolemgt0  13902