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  4434  smodm  6358  erdm  6611  ixpfn  6772  dif1en  6949  eluzelz  9627  elfz3nn0  10207  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  bitsss  12127  gznegcl  12569  gzcjcl  12570  gzaddcl  12571  gzmulcl  12572  gzabssqcl  12575  4sqlem4a  12585  xpsff1o  13051  subgss  13380  rngmgp  13568  srgmgp  13600  ringmgp  13634  lmodring  13927  lmodprop2d  13980  reeff1oleme  15092  cosq14gt0  15152  cosq23lt0  15153  coseq0q4123  15154  coseq00topi  15155  coseq0negpitopi  15156  cosq34lt1  15170  cos02pilt1  15171  ioocosf1o  15174  gausslemma2dlem1a  15383  2sqlem2  15440  2sqlem3  15442