Theorem simp2bi 1044

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
simp2bi	|- ( ph -> ch )

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 120	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp2d 1041	1 |- ( ph -> ch )

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  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  0ellim  4538  smodm  6552  erdm  6807  ixpfn  6976  dif1en  7173  eluzelz  9910  lincmble  10385  elfz3nn0  10500  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  bitsss  12690  gznegcl  13132  gzcjcl  13133  gzaddcl  13134  gzmulcl  13135  gzabssqcl  13138  4sqlem4a  13148  xpsff1o  13647  subgss  13954  rngmgp  14210  srgmgp  14246  ringmgp  14280  lmodring  14604  lmodprop2d  14657  reeff1oleme  15796  cosq14gt0  15856  cosq23lt0  15857  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  cosq34lt1  15874  cos02pilt1  15875  ioocosf1o  15878  gausslemma2dlem1a  16091  2sqlem2  16148  2sqlem3  16150