Theorem simp2bi 1015

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

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

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 982

This theorem is referenced by:  0ellim  4423  smodm  6324  erdm  6577  ixpfn  6738  dif1en  6915  eluzelz  9578  elfz3nn0  10157  ef01bndlem  11811  sin01bnd  11812  cos01bnd  11813  sin01gt0  11816  gznegcl  12424  gzcjcl  12425  gzaddcl  12426  gzmulcl  12427  gzabssqcl  12430  4sqlem4a  12440  xpsff1o  12843  subgss  13146  rngmgp  13325  srgmgp  13357  ringmgp  13391  lmodring  13654  lmodprop2d  13707  reeff1oleme  14731  cosq14gt0  14791  cosq23lt0  14792  coseq0q4123  14793  coseq00topi  14794  coseq0negpitopi  14795  cosq34lt1  14809  cos02pilt1  14810  ioocosf1o  14813  2sqlem2  15001  2sqlem3  15003