Theorem simp1bi 1014

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

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

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 982

This theorem is referenced by:  limord  4413  smores2  6319  smofvon2dm  6321  smofvon  6324  errel  6568  lincmb01cmp  10033  iccf1o  10034  elfznn0  10144  elfzouz  10181  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  sin01gt0  11801  cos01gt0  11802  sin02gt0  11803  eulerthlema  12262  modprm0  12286  gzcn  12404  subgbas  13117  subgrcl  13118  rngabl  13289  srgcmn  13320  ringgrp  13355  subrngrcl  13550  lmodgrp  13610  coseq00topi  14713  coseq0negpitopi  14714  cosq34lt1  14728  cos11  14731  nconstwlpolemgt0  15271