Theorem simp3bi 1038

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

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

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 1004

This theorem is referenced by:  limuni  4486  smores2  6438  ersym  6690  ertr  6693  fvixp  6848  en2  6971  fiintim  7089  eluzle  9730  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  gznegcl  12893  gzcjcl  12894  gzaddcl  12895  gzmulcl  12896  gzabssqcl  12899  4sqlem4a  12909  ennnfonelemim  12990  prdsbasprj  13310  xpsff1o  13377  subggrp  13709  srgdilem  13927  srgrz  13942  srglz  13943  ringdilem  13970  ringsrg  14005  subrngss  14158  lmodlema  14250  reeff1oleme  15440  cosq14gt0  15500  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  cosq34lt1  15518  cos02pilt1  15519  ioocosf1o  15522  2sqlem2  15788  2sqlem3  15790