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  4442  smores2  6380  smofvon2dm  6382  smofvon  6385  errel  6629  lincmb01cmp  10125  iccf1o  10126  elfznn0  10236  elfzouz  10273  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  sin01gt0  12073  cos01gt0  12074  sin02gt0  12075  eulerthlema  12552  modprm0  12577  gzcn  12695  subgbas  13514  subgrcl  13515  rngabl  13697  srgcmn  13728  ringgrp  13763  subrngrcl  13965  lmodgrp  14056  coseq00topi  15307  coseq0negpitopi  15308  cosq34lt1  15322  cos11  15325  nconstwlpolemgt0  16003