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  4501  smodm  6500  erdm  6755  ixpfn  6916  dif1en  7111  eluzelz  9809  lincmble  10283  elfz3nn0  10395  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  bitsss  12569  gznegcl  13011  gzcjcl  13012  gzaddcl  13013  gzmulcl  13014  gzabssqcl  13017  4sqlem4a  13027  xpsff1o  13495  subgss  13824  rngmgp  14013  srgmgp  14045  ringmgp  14079  lmodring  14374  lmodprop2d  14427  reeff1oleme  15566  cosq14gt0  15626  cosq23lt0  15627  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  cosq34lt1  15644  cos02pilt1  15645  ioocosf1o  15648  gausslemma2dlem1a  15860  2sqlem2  15917  2sqlem3  15919