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  9944  lincmble  10417  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  gznegcl  13177  gzcjcl  13178  gzaddcl  13179  gzmulcl  13180  gzabssqcl  13183  4sqlem4a  13193  ennnfonelemim  13367  xpsff1o  13723  subggrp  14033  prdsbasprj  14266  srgdilem  14357  srgrz  14372  srglz  14373  ringdilem  14400  ringsrg  14436  subrngss  14592  lmodlema  14712  reeff1oleme  15964  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  cosq34lt1  16043  cos02pilt1  16044  ioocosf1o  16047  2sqlem2  16400  2sqlem3  16402