Theorem simp2bi 1015

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

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

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 982

This theorem is referenced by:  0ellim  4444  smodm  6376  erdm  6629  ixpfn  6790  dif1en  6975  eluzelz  9656  elfz3nn0  10236  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  bitsss  12198  gznegcl  12640  gzcjcl  12641  gzaddcl  12642  gzmulcl  12643  gzabssqcl  12646  4sqlem4a  12656  xpsff1o  13123  subgss  13452  rngmgp  13640  srgmgp  13672  ringmgp  13706  lmodring  13999  lmodprop2d  14052  reeff1oleme  15186  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  cosq34lt1  15264  cos02pilt1  15265  ioocosf1o  15268  gausslemma2dlem1a  15477  2sqlem2  15534  2sqlem3  15536