Theorem simp3bi 999

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

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

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 965

This theorem is referenced by:  limuni  4326  smores2  6199  ersym  6449  ertr  6452  fvixp  6605  fiintim  6825  eluzle  9362  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  ennnfonelemim  11973  reeff1oleme  12901  cosq14gt0  12961  cosq23lt0  12962  coseq0q4123  12963  coseq00topi  12964  coseq0negpitopi  12965  cosq34lt1  12979  cos02pilt1  12980  ioocosf1o  12983