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  10405  lincmble  10406  iccf1o  10407  elfznn0  10521  elfzouz  10558  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  eulerthlema  13008  modprm0  13033  gzcn  13151  ballotfilemscr  13262  ballotfilemrinv0  13276  subgbas  13981  subgrcl  13982  rngabl  14234  srgcmn  14270  ringgrp  14305  subrngrcl  14511  lmodgrp  14630  coseq00topi  15936  coseq0negpitopi  15937  cosq34lt1  15951  cos11  15954  clwwlkbp  16636  clwwlksswrd  16638  nconstwlpolemgt0  17114