Theorem simp1bi 1036

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

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

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 1004

This theorem is referenced by:  limord  4490  smores2  6455  smofvon2dm  6457  smofvon  6460  errel  6706  lincmb01cmp  10228  iccf1o  10229  elfznn0  10339  elfzouz  10376  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  eulerthlema  12792  modprm0  12817  gzcn  12935  subgbas  13755  subgrcl  13756  rngabl  13938  srgcmn  13969  ringgrp  14004  subrngrcl  14207  lmodgrp  14298  coseq00topi  15549  coseq0negpitopi  15550  cosq34lt1  15564  cos11  15567  clwwlkbp  16190  clwwlksswrd  16192  nconstwlpolemgt0  16604