Theorem simp3bi 998

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

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

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 964

This theorem is referenced by:  limuni  4313  smores2  6184  ersym  6434  ertr  6437  fvixp  6590  fiintim  6810  eluzle  9331  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  sin01gt0  11457  ennnfonelemim  11926  cosq14gt0  12902  cosq23lt0  12903  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  cosq34lt1  12920  cos02pilt1  12921