Theorem simp3bi 1038

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

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

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 1004

This theorem is referenced by:  limuni  4491  smores2  6455  ersym  6709  ertr  6712  fvixp  6867  en2  6993  fiintim  7116  eluzle  9758  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  gznegcl  12938  gzcjcl  12939  gzaddcl  12940  gzmulcl  12941  gzabssqcl  12944  4sqlem4a  12954  ennnfonelemim  13035  prdsbasprj  13355  xpsff1o  13422  subggrp  13754  srgdilem  13972  srgrz  13987  srglz  13988  ringdilem  14015  ringsrg  14050  subrngss  14204  lmodlema  14296  reeff1oleme  15486  cosq14gt0  15546  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  cosq34lt1  15564  cos02pilt1  15565  ioocosf1o  15568  2sqlem2  15834  2sqlem3  15836