Theorem simp1bi 1015

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

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

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 983

This theorem is referenced by:  limord  4460  smores2  6403  smofvon2dm  6405  smofvon  6408  errel  6652  lincmb01cmp  10160  iccf1o  10161  elfznn0  10271  elfzouz  10308  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  sin01gt0  12188  cos01gt0  12189  sin02gt0  12190  eulerthlema  12667  modprm0  12692  gzcn  12810  subgbas  13629  subgrcl  13630  rngabl  13812  srgcmn  13843  ringgrp  13878  subrngrcl  14080  lmodgrp  14171  coseq00topi  15422  coseq0negpitopi  15423  cosq34lt1  15437  cos11  15440  nconstwlpolemgt0  16205