Theorem simp3bi 1016

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

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

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 982

This theorem is referenced by:  limuni  4442  smores2  6379  ersym  6631  ertr  6634  fvixp  6789  en2  6911  fiintim  7027  eluzle  9659  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  gznegcl  12640  gzcjcl  12641  gzaddcl  12642  gzmulcl  12643  gzabssqcl  12646  4sqlem4a  12656  ennnfonelemim  12737  prdsbasprj  13056  xpsff1o  13123  subggrp  13455  srgdilem  13673  srgrz  13688  srglz  13689  ringdilem  13716  ringsrg  13751  subrngss  13904  lmodlema  13996  reeff1oleme  15186  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  cosq34lt1  15264  cos02pilt1  15265  ioocosf1o  15268  2sqlem2  15534  2sqlem3  15536