Theorem simp3bi 1014

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 120	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp3d 1011	1 |- ( ph -> th )

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

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  limuni  4396  smores2  6294  ersym  6546  ertr  6549  fvixp  6702  fiintim  6927  eluzle  9539  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  gznegcl  12372  gzcjcl  12373  gzaddcl  12374  gzmulcl  12375  gzabssqcl  12378  4sqlem4a  12388  ennnfonelemim  12424  xpsff1o  12767  subggrp  13035  srgdilem  13150  srgrz  13165  srglz  13166  ringdilem  13193  ringsrg  13222  lmodlema  13380  reeff1oleme  14163  cosq14gt0  14223  cosq23lt0  14224  coseq0q4123  14225  coseq00topi  14226  coseq0negpitopi  14227  cosq34lt1  14241  cos02pilt1  14242  ioocosf1o  14245  2sqlem2  14432  2sqlem3  14434