Theorem simp1bi 1012

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

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

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 980

This theorem is referenced by:  limord  4395  smores2  6294  smofvon2dm  6296  smofvon  6299  errel  6543  lincmb01cmp  10002  iccf1o  10003  elfznn0  10113  elfzouz  10150  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  eulerthlema  12229  modprm0  12253  gzcn  12369  subgbas  13036  subgrcl  13037  srgcmn  13147  ringgrp  13182  lmodgrp  13382  coseq00topi  14226  coseq0negpitopi  14227  cosq34lt1  14241  cos11  14244  nconstwlpolemgt0  14781