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  4428  smores2  6349  ersym  6601  ertr  6604  fvixp  6759  fiintim  6987  eluzle  9607  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  gznegcl  12516  gzcjcl  12517  gzaddcl  12518  gzmulcl  12519  gzabssqcl  12522  4sqlem4a  12532  ennnfonelemim  12584  xpsff1o  12935  subggrp  13250  srgdilem  13468  srgrz  13483  srglz  13484  ringdilem  13511  ringsrg  13546  subrngss  13699  lmodlema  13791  reeff1oleme  14948  cosq14gt0  15008  cosq23lt0  15009  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  cosq34lt1  15026  cos02pilt1  15027  ioocosf1o  15030  2sqlem2  15272  2sqlem3  15274