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  4516  smores2  6525  smofvon2dm  6527  smofvon  6530  errel  6776  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  elfznn0  10448  elfzouz  10485  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  eulerthlema  12927  modprm0  12952  gzcn  13070  subgbas  13895  subgrcl  13896  rngabl  14079  srgcmn  14110  ringgrp  14145  subrngrcl  14348  lmodgrp  14442  coseq00topi  15700  coseq0negpitopi  15701  cosq34lt1  15715  cos11  15718  clwwlkbp  16390  clwwlksswrd  16392  nconstwlpolemgt0  16850