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  9934  lincmble  10406  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  gznegcl  13154  gzcjcl  13155  gzaddcl  13156  gzmulcl  13157  gzabssqcl  13160  4sqlem4a  13170  ennnfonelemim  13315  xpsff1o  13670  subggrp  13980  prdsbasprj  14182  srgdilem  14273  srgrz  14288  srglz  14289  ringdilem  14316  ringsrg  14352  subrngss  14508  lmodlema  14628  reeff1oleme  15873  cosq14gt0  15933  cosq23lt0  15934  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  cosq34lt1  15951  cos02pilt1  15952  ioocosf1o  15955  2sqlem2  16234  2sqlem3  16236