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  9940  lincmble  10416  elfz3nn0  10532  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  bitsss  12728  gznegcl  13174  gzcjcl  13175  gzaddcl  13176  gzmulcl  13177  gzabssqcl  13180  4sqlem4a  13190  xpsff1o  13719  subgss  14026  rngmgp  14284  srgmgp  14321  ringmgp  14355  lmodring  14680  lmodprop2d  14734  reeff1oleme  15922  cosq14gt0  15983  cosq23lt0  15984  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  cosq34lt1  16001  cos02pilt1  16002  ioocosf1o  16005  gausslemma2dlem1a  16275  2sqlem2  16332  2sqlem3  16334