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  4519  smodm  6522  erdm  6777  ixpfn  6939  dif1en  7136  eluzelz  9863  lincmble  10337  elfz3nn0  10449  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  bitsss  12631  gznegcl  13073  gzcjcl  13074  gzaddcl  13075  gzmulcl  13076  gzabssqcl  13079  4sqlem4a  13089  xpsff1o  13562  subgss  13891  rngmgp  14080  srgmgp  14112  ringmgp  14146  lmodring  14443  lmodprop2d  14496  reeff1oleme  15637  cosq14gt0  15697  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  cosq34lt1  15715  cos02pilt1  15716  ioocosf1o  15719  gausslemma2dlem1a  15931  2sqlem2  15988  2sqlem3  15990