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  4498  smores2  6503  smofvon2dm  6505  smofvon  6508  errel  6754  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  elfznn0  10394  elfzouz  10431  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  eulerthlema  12865  modprm0  12890  gzcn  13008  subgbas  13828  subgrcl  13829  rngabl  14012  srgcmn  14043  ringgrp  14078  subrngrcl  14281  lmodgrp  14373  coseq00topi  15629  coseq0negpitopi  15630  cosq34lt1  15644  cos11  15647  clwwlkbp  16319  clwwlksswrd  16321  nconstwlpolemgt0  16780