Theorem simp3bi 1009

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

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

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 975

This theorem is referenced by:  limuni  4381  smores2  6273  ersym  6525  ertr  6528  fvixp  6681  fiintim  6906  eluzle  9499  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  gznegcl  12327  gzcjcl  12328  gzaddcl  12329  gzmulcl  12330  gzabssqcl  12333  4sqlem4a  12343  ennnfonelemim  12379  reeff1oleme  13487  cosq14gt0  13547  cosq23lt0  13548  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  cosq34lt1  13565  cos02pilt1  13566  ioocosf1o  13569  2sqlem2  13745  2sqlem3  13747