Theorem simp1bi 1014

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

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

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 982

This theorem is referenced by:  limord  4427  smores2  6349  smofvon2dm  6351  smofvon  6354  errel  6598  lincmb01cmp  10072  iccf1o  10073  elfznn0  10183  elfzouz  10220  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  eulerthlema  12371  modprm0  12395  gzcn  12513  subgbas  13251  subgrcl  13252  rngabl  13434  srgcmn  13465  ringgrp  13500  subrngrcl  13702  lmodgrp  13793  coseq00topi  15011  coseq0negpitopi  15012  cosq34lt1  15026  cos11  15029  nconstwlpolemgt0  15624