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  4441  smores2  6379  smofvon2dm  6381  smofvon  6384  errel  6628  lincmb01cmp  10124  iccf1o  10125  elfznn0  10235  elfzouz  10272  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  sin01gt0  12044  cos01gt0  12045  sin02gt0  12046  eulerthlema  12523  modprm0  12548  gzcn  12666  subgbas  13485  subgrcl  13486  rngabl  13668  srgcmn  13699  ringgrp  13734  subrngrcl  13936  lmodgrp  14027  coseq00topi  15278  coseq0negpitopi  15279  cosq34lt1  15293  cos11  15296  nconstwlpolemgt0  15965