Theorem simp2bi 1039

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

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

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 1006

This theorem is referenced by:  0ellim  4495  smodm  6457  erdm  6712  ixpfn  6873  dif1en  7068  eluzelz  9765  elfz3nn0  10350  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  bitsss  12524  gznegcl  12966  gzcjcl  12967  gzaddcl  12968  gzmulcl  12969  gzabssqcl  12972  4sqlem4a  12982  xpsff1o  13450  subgss  13779  rngmgp  13968  srgmgp  14000  ringmgp  14034  lmodring  14328  lmodprop2d  14381  reeff1oleme  15515  cosq14gt0  15575  cosq23lt0  15576  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  cosq34lt1  15593  cos02pilt1  15594  ioocosf1o  15597  gausslemma2dlem1a  15806  2sqlem2  15863  2sqlem3  15865