Theorem simp1bi 1036

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 120	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 1033	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  limord  4486  smores2  6446  smofvon2dm  6448  smofvon  6451  errel  6697  lincmb01cmp  10211  iccf1o  10212  elfznn0  10322  elfzouz  10359  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  eulerthlema  12767  modprm0  12792  gzcn  12910  subgbas  13730  subgrcl  13731  rngabl  13913  srgcmn  13944  ringgrp  13979  subrngrcl  14182  lmodgrp  14273  coseq00topi  15524  coseq0negpitopi  15525  cosq34lt1  15539  cos11  15542  clwwlkbp  16133  clwwlksswrd  16135  nconstwlpolemgt0  16492