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  4517  smores2  6525  ersym  6779  ertr  6782  fvixp  6938  en2  7065  fiintim  7191  eluzle  9866  lincmble  10337  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  gznegcl  13073  gzcjcl  13074  gzaddcl  13075  gzmulcl  13076  gzabssqcl  13079  4sqlem4a  13089  ennnfonelemim  13175  prdsbasprj  13495  xpsff1o  13562  subggrp  13894  srgdilem  14113  srgrz  14128  srglz  14129  ringdilem  14156  ringsrg  14191  subrngss  14345  lmodlema  14440  reeff1oleme  15637  cosq14gt0  15697  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  cosq34lt1  15715  cos02pilt1  15716  ioocosf1o  15719  2sqlem2  15988  2sqlem3  15990