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  4378  smores2  6270  smofvon2dm  6272  smofvon  6275  errel  6518  lincmb01cmp  9947  iccf1o  9948  elfznn0  10057  elfzouz  10094  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  sin01gt0  11711  cos01gt0  11712  sin02gt0  11713  eulerthlema  12171  modprm0  12195  gzcn  12311  coseq00topi  13509  coseq0negpitopi  13510  cosq34lt1  13524  cos11  13527  nconstwlpolemgt0  14055