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  4542  smores2  6569  smofvon2dm  6571  smofvon  6574  errel  6820  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  elfznn0  10538  elfzouz  10575  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  eulerthlema  13037  modprm0  13062  gzcn  13180  ballotfilemscr  13320  ballotfilemrinv0  13334  subgbas  14040  subgrcl  14041  rngabl  14341  srgcmn  14377  ringgrp  14412  subrngrcl  14620  lmodgrp  14739  coseq00topi  16062  coseq0negpitopi  16063  cosq34lt1  16078  cos11  16081  clwwlkbp  16841  clwwlksswrd  16843  nconstwlpolemgt0  17321