Theorem simp1bi 1043

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limord  4540  smores2  6565  smofvon2dm  6567  smofvon  6570  errel  6816  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  elfznn0  10531  elfzouz  10568  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  eulerthlema  13028  modprm0  13053  gzcn  13171  ballotfilemscr  13311  ballotfilemrinv0  13325  subgbas  14030  subgrcl  14031  rngabl  14283  srgcmn  14319  ringgrp  14354  subrngrcl  14560  lmodgrp  14679  coseq00topi  15986  coseq0negpitopi  15987  cosq34lt1  16001  cos11  16004  clwwlkbp  16734  clwwlksswrd  16736  nconstwlpolemgt0  17212