Theorem simp1bi 1007

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

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

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 975

This theorem is referenced by:  limord  4380  smores2  6273  smofvon2dm  6275  smofvon  6278  errel  6522  lincmb01cmp  9960  iccf1o  9961  elfznn0  10070  elfzouz  10107  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  eulerthlema  12184  modprm0  12208  gzcn  12324  coseq00topi  13550  coseq0negpitopi  13551  cosq34lt1  13565  cos11  13568  nconstwlpolemgt0  14095