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  6459  smofvon2dm  6461  smofvon  6464  errel  6710  lincmb01cmp  10237  iccf1o  10238  elfznn0  10348  elfzouz  10385  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  eulerthlema  12801  modprm0  12826  gzcn  12944  subgbas  13764  subgrcl  13765  rngabl  13947  srgcmn  13978  ringgrp  14013  subrngrcl  14216  lmodgrp  14307  coseq00topi  15558  coseq0negpitopi  15559  cosq34lt1  15573  cos11  15576  clwwlkbp  16245  clwwlksswrd  16247  nconstwlpolemgt0  16668