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  4493  smodm  6452  erdm  6707  ixpfn  6868  dif1en  7061  eluzelz  9755  elfz3nn0  10340  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  bitsss  12496  gznegcl  12938  gzcjcl  12939  gzaddcl  12940  gzmulcl  12941  gzabssqcl  12944  4sqlem4a  12954  xpsff1o  13422  subgss  13751  rngmgp  13939  srgmgp  13971  ringmgp  14005  lmodring  14299  lmodprop2d  14352  reeff1oleme  15486  cosq14gt0  15546  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  cosq34lt1  15564  cos02pilt1  15565  ioocosf1o  15568  gausslemma2dlem1a  15777  2sqlem2  15834  2sqlem3  15836