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  4485  smores2  6438  smofvon2dm  6440  smofvon  6443  errel  6687  lincmb01cmp  10195  iccf1o  10196  elfznn0  10306  elfzouz  10343  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  eulerthlema  12747  modprm0  12772  gzcn  12890  subgbas  13710  subgrcl  13711  rngabl  13893  srgcmn  13924  ringgrp  13959  subrngrcl  14161  lmodgrp  14252  coseq00topi  15503  coseq0negpitopi  15504  cosq34lt1  15518  cos11  15521  nconstwlpolemgt0  16391