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  10416  lincmble  10417  iccf1o  10418  elfznn0  10532  elfzouz  10569  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  eulerthlema  13031  modprm0  13056  gzcn  13174  ballotfilemscr  13314  ballotfilemrinv0  13328  subgbas  14034  subgrcl  14035  rngabl  14318  srgcmn  14354  ringgrp  14389  subrngrcl  14595  lmodgrp  14714  coseq00topi  16028  coseq0negpitopi  16029  cosq34lt1  16043  cos11  16046  clwwlkbp  16802  clwwlksswrd  16804  nconstwlpolemgt0  17281