Theorem simp2bi 1040

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

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

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 1007

This theorem is referenced by:  0ellim  4524  smodm  6535  erdm  6790  ixpfn  6952  dif1en  7149  eluzelz  9881  lincmble  10356  elfz3nn0  10471  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  bitsss  12656  gznegcl  13098  gzcjcl  13099  gzaddcl  13100  gzmulcl  13101  gzabssqcl  13104  4sqlem4a  13114  xpsff1o  13613  subgss  13927  rngmgp  14175  srgmgp  14211  ringmgp  14245  lmodring  14569  lmodprop2d  14622  reeff1oleme  15763  cosq14gt0  15823  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  cosq34lt1  15841  cos02pilt1  15842  ioocosf1o  15845  gausslemma2dlem1a  16057  2sqlem2  16114  2sqlem3  16116