Theorem simp1bi 1038

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

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

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 1006

This theorem is referenced by:  limord  4492  smores2  6460  smofvon2dm  6462  smofvon  6465  errel  6711  lincmb01cmp  10238  iccf1o  10239  elfznn0  10349  elfzouz  10386  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  eulerthlema  12820  modprm0  12845  gzcn  12963  subgbas  13783  subgrcl  13784  rngabl  13967  srgcmn  13998  ringgrp  14033  subrngrcl  14236  lmodgrp  14327  coseq00topi  15578  coseq0negpitopi  15579  cosq34lt1  15593  cos11  15596  clwwlkbp  16265  clwwlksswrd  16267  nconstwlpolemgt0  16720