Theorem simp2bi 1008

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

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

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 975

This theorem is referenced by:  0ellim  4383  smodm  6270  erdm  6523  ixpfn  6682  dif1en  6857  eluzelz  9496  elfz3nn0  10071  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  gznegcl  12327  gzcjcl  12328  gzaddcl  12329  gzmulcl  12330  gzabssqcl  12333  4sqlem4a  12343  reeff1oleme  13487  cosq14gt0  13547  cosq23lt0  13548  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  cosq34lt1  13565  cos02pilt1  13566  ioocosf1o  13569  2sqlem2  13745  2sqlem3  13747