Theorem simp3bi 1045

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limuni  4541  smores2  6565  ersym  6819  ertr  6822  fvixp  6985  en2  7112  fiintim  7238  eluzle  9943  lincmble  10416  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  gznegcl  13174  gzcjcl  13175  gzaddcl  13176  gzmulcl  13177  gzabssqcl  13180  4sqlem4a  13190  ennnfonelemim  13364  xpsff1o  13719  subggrp  14029  prdsbasprj  14231  srgdilem  14322  srgrz  14337  srglz  14338  ringdilem  14365  ringsrg  14401  subrngss  14557  lmodlema  14677  reeff1oleme  15922  cosq14gt0  15983  cosq23lt0  15984  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  cosq34lt1  16001  cos02pilt1  16002  ioocosf1o  16005  2sqlem2  16332  2sqlem3  16334