Theorem simp2bi 1044

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  0ellim  4543  smodm  6562  erdm  6817  ixpfn  6986  dif1en  7183  eluzelz  9941  lincmble  10417  elfz3nn0  10533  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  bitsss  12731  gznegcl  13177  gzcjcl  13178  gzaddcl  13179  gzmulcl  13180  gzabssqcl  13183  4sqlem4a  13193  xpsff1o  13723  subgss  14030  rngmgp  14319  srgmgp  14356  ringmgp  14390  lmodring  14715  lmodprop2d  14769  reeff1oleme  15964  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  cosq34lt1  16043  cos02pilt1  16044  ioocosf1o  16047  gausslemma2dlem1a  16343  2sqlem2  16400  2sqlem3  16402