Theorem simp3bi 1017

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

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

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 983

This theorem is referenced by:  limuni  4443  smores2  6380  ersym  6632  ertr  6635  fvixp  6790  en2  6912  fiintim  7028  eluzle  9660  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  sin01gt0  12073  gznegcl  12698  gzcjcl  12699  gzaddcl  12700  gzmulcl  12701  gzabssqcl  12704  4sqlem4a  12714  ennnfonelemim  12795  prdsbasprj  13114  xpsff1o  13181  subggrp  13513  srgdilem  13731  srgrz  13746  srglz  13747  ringdilem  13774  ringsrg  13809  subrngss  13962  lmodlema  14054  reeff1oleme  15244  cosq14gt0  15304  cosq23lt0  15305  coseq0q4123  15306  coseq00topi  15307  coseq0negpitopi  15308  cosq34lt1  15322  cos02pilt1  15323  ioocosf1o  15326  2sqlem2  15592  2sqlem3  15594