Theorem simp1bi 1012

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

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

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 980

This theorem is referenced by:  limord  4397  smores2  6297  smofvon2dm  6299  smofvon  6302  errel  6546  lincmb01cmp  10005  iccf1o  10006  elfznn0  10116  elfzouz  10153  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  eulerthlema  12232  modprm0  12256  gzcn  12372  subgbas  13043  subgrcl  13044  srgcmn  13154  ringgrp  13189  lmodgrp  13389  coseq00topi  14295  coseq0negpitopi  14296  cosq34lt1  14310  cos11  14313  nconstwlpolemgt0  14851