Theorem simp1bi 1043

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

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

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 1011

This theorem is referenced by:  limord  4535  smores2  6555  smofvon2dm  6557  smofvon  6560  errel  6806  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  elfznn0  10499  elfzouz  10536  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  eulerthlema  12986  modprm0  13011  gzcn  13129  ballotfilemscr  13240  ballotfilemrinv0  13254  subgbas  13958  subgrcl  13959  rngabl  14209  srgcmn  14244  ringgrp  14279  subrngrcl  14484  lmodgrp  14603  coseq00topi  15859  coseq0negpitopi  15860  cosq34lt1  15874  cos11  15877  clwwlkbp  16550  clwwlksswrd  16552  nconstwlpolemgt0  17019