Theorem simp2bi 997

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

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

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 964

This theorem is referenced by:  0ellim  4320  smodm  6188  erdm  6439  ixpfn  6598  dif1en  6773  eluzelz  9335  elfz3nn0  9895  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cosq14gt0  12913  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  cosq34lt1  12931  cos02pilt1  12932