Theorem simp3bi 1041

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

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

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 1007

This theorem is referenced by:  limuni  4522  smores2  6538  ersym  6792  ertr  6795  fvixp  6951  en2  7078  fiintim  7204  eluzle  9884  lincmble  10356  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  gznegcl  13098  gzcjcl  13099  gzaddcl  13100  gzmulcl  13101  gzabssqcl  13104  4sqlem4a  13114  ennnfonelemim  13259  xpsff1o  13613  subggrp  13930  prdsbasprj  14124  srgdilem  14212  srgrz  14227  srglz  14228  ringdilem  14255  ringsrg  14290  subrngss  14446  lmodlema  14566  reeff1oleme  15763  cosq14gt0  15823  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  cosq34lt1  15841  cos02pilt1  15842  ioocosf1o  15845  2sqlem2  16114  2sqlem3  16116