Theorem simp1bi 1039

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

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

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 1007

This theorem is referenced by:  limord  4521  smores2  6538  smofvon2dm  6540  smofvon  6543  errel  6789  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  elfznn0  10470  elfzouz  10507  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  eulerthlema  12952  modprm0  12977  gzcn  13095  ballotfilemscr  13206  ballotfilemrinv0  13220  subgbas  13931  subgrcl  13932  rngabl  14174  srgcmn  14209  ringgrp  14244  subrngrcl  14449  lmodgrp  14568  coseq00topi  15826  coseq0negpitopi  15827  cosq34lt1  15841  cos11  15844  clwwlkbp  16516  clwwlksswrd  16518  nconstwlpolemgt0  16976