Theorem simp3bi 1040

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

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

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 1006

This theorem is referenced by:  limuni  4493  smores2  6460  ersym  6714  ertr  6717  fvixp  6872  en2  6998  fiintim  7123  eluzle  9768  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  gznegcl  12966  gzcjcl  12967  gzaddcl  12968  gzmulcl  12969  gzabssqcl  12972  4sqlem4a  12982  ennnfonelemim  13063  prdsbasprj  13383  xpsff1o  13450  subggrp  13782  srgdilem  14001  srgrz  14016  srglz  14017  ringdilem  14044  ringsrg  14079  subrngss  14233  lmodlema  14325  reeff1oleme  15515  cosq14gt0  15575  cosq23lt0  15576  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  cosq34lt1  15593  cos02pilt1  15594  ioocosf1o  15597  2sqlem2  15863  2sqlem3  15865