Theorem simp2bi 998

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 119	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp2d 995	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  0ellim  4328  smodm  6196  erdm  6447  ixpfn  6606  dif1en  6781  eluzelz  9359  elfz3nn0  9926  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  reeff1oleme  12901  cosq14gt0  12961  cosq23lt0  12962  coseq0q4123  12963  coseq00topi  12964  coseq0negpitopi  12965  cosq34lt1  12979  cos02pilt1  12980  ioocosf1o  12983