Theorem simp2bi 1037

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

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

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 1004

This theorem is referenced by:  0ellim  4488  smodm  6435  erdm  6688  ixpfn  6849  dif1en  7037  eluzelz  9727  elfz3nn0  10307  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  bitsss  12451  gznegcl  12893  gzcjcl  12894  gzaddcl  12895  gzmulcl  12896  gzabssqcl  12899  4sqlem4a  12909  xpsff1o  13377  subgss  13706  rngmgp  13894  srgmgp  13926  ringmgp  13960  lmodring  14253  lmodprop2d  14306  reeff1oleme  15440  cosq14gt0  15500  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  cosq34lt1  15518  cos02pilt1  15519  ioocosf1o  15522  gausslemma2dlem1a  15731  2sqlem2  15788  2sqlem3  15790