Theorem simp3bi 1004

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
simp3bi	|- ( ph -> th )

Proof of Theorem simp3bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 119	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp3d 1001	1 |- ( ph -> th )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  limuni  4374  smores2  6262  ersym  6513  ertr  6516  fvixp  6669  fiintim  6894  eluzle  9478  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  gznegcl  12305  gzcjcl  12306  gzaddcl  12307  gzmulcl  12308  gzabssqcl  12311  4sqlem4a  12321  ennnfonelemim  12357  reeff1oleme  13333  cosq14gt0  13393  cosq23lt0  13394  coseq0q4123  13395  coseq00topi  13396  coseq0negpitopi  13397  cosq34lt1  13411  cos02pilt1  13412  ioocosf1o  13415  2sqlem2  13591  2sqlem3  13593