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  4499  smores2  6503  ersym  6757  ertr  6760  fvixp  6915  en2  7041  fiintim  7166  eluzle  9812  lincmble  10283  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  gznegcl  13011  gzcjcl  13012  gzaddcl  13013  gzmulcl  13014  gzabssqcl  13017  4sqlem4a  13027  ennnfonelemim  13108  prdsbasprj  13428  xpsff1o  13495  subggrp  13827  srgdilem  14046  srgrz  14061  srglz  14062  ringdilem  14089  ringsrg  14124  subrngss  14278  lmodlema  14371  reeff1oleme  15566  cosq14gt0  15626  cosq23lt0  15627  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  cosq34lt1  15644  cos02pilt1  15645  ioocosf1o  15648  2sqlem2  15917  2sqlem3  15919