Theorem simp1bi 1014

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

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

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 982

This theorem is referenced by:  limord  4426  smores2  6347  smofvon2dm  6349  smofvon  6352  errel  6596  lincmb01cmp  10069  iccf1o  10070  elfznn0  10180  elfzouz  10217  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  eulerthlema  12368  modprm0  12392  gzcn  12510  subgbas  13248  subgrcl  13249  rngabl  13431  srgcmn  13462  ringgrp  13497  subrngrcl  13699  lmodgrp  13790  coseq00topi  14970  coseq0negpitopi  14971  cosq34lt1  14985  cos11  14988  nconstwlpolemgt0  15554