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 )

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

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 1011

This theorem is referenced by:  limuni  4536  smores2  6555  ersym  6809  ertr  6812  fvixp  6975  en2  7102  fiintim  7228  eluzle  9913  lincmble  10385  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  gznegcl  13132  gzcjcl  13133  gzaddcl  13134  gzmulcl  13135  gzabssqcl  13138  4sqlem4a  13148  ennnfonelemim  13293  xpsff1o  13647  subggrp  13957  prdsbasprj  14159  srgdilem  14247  srgrz  14262  srglz  14263  ringdilem  14290  ringsrg  14325  subrngss  14481  lmodlema  14601  reeff1oleme  15796  cosq14gt0  15856  cosq23lt0  15857  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  cosq34lt1  15874  cos02pilt1  15875  ioocosf1o  15878  2sqlem2  16148  2sqlem3  16150