Theorem simp1bi 972

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
simp1bi	|- ( ph -> ps )

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 |- ( ph <-> ( ps /\ ch /\ th ) )
2	1	biimpi 187	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 969	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 177   /\ w3a 936

This theorem is referenced by:  limord  4600  smores2  6575  smofvon2  6577  smofvon  6580  errel  6873  lincmb01cmp  10994  iccf1o  10995  elfznn0  11039  elfzouz  11099  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  smueqlem  12957  gzcn  13255  mresspw  13772  drsprs  14348  ipodrscl  14543  subgrcl  14904  pgpprm  15182  slwprm  15198  efgsdmi  15319  efgsrel  15321  efgs1b  15323  efgsp1  15324  efgsres  15325  efgsfo  15326  efgredlema  15327  efgredlemf  15328  efgredlemd  15331  efgredlemc  15332  efgredlem  15334  efgrelexlemb  15337  efgcpbllemb  15342  rnggrp  15624  irredcl  15764  lmodgrp  15912  lssss  15968  phllvec  16815  obsrcl  16905  fclstop  17996  tmdmnd  18058  tgpgrp  18061  trgtgp  18150  tdrgtrg  18155  ust0  18202  ngpgrp  18599  elii1  18913  elii2  18914  icopnfcnv  18920  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  oprpiece1res1  18929  oprpiece1res2  18930  phtpcer  18973  pcoval2  18994  pcoass  19002  clmlmod  19045  cphphl  19087  cphnlm  19088  cphsca  19095  bnnvc  19246  uc1pcl  20019  mon1pcl  20020  sinq12ge0  20369  cosq14ge0  20372  cosord  20387  cos11  20388  recosf1o  20390  resinf1o  20391  efifo  20402  logrncn  20413  atanf  20673  atanneg  20700  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  areass  20751  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  subgores  21845  subgoid  21848  subgoinv  21849  sticl  23671  hstcl  23673  ofldfld  24189  elunitrn  24248  brbtwn2  25748  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3  25774  ax5seglem5  25776  ax5seglem6  25777  ax5seglem9  25780  ax5seg  25781  axbtwnid  25782  axpaschlem  25783  axpasch  25784  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  locfintop  26270  pmtrfconj  27275  stoweidlem60  27676  2spotiundisj  28165  bnj564  28818  bnj1366  28907  bnj545  28972  bnj548  28974  bnj558  28979  bnj570  28982  bnj580  28990  bnj929  29013  bnj998  29033  bnj1006  29036  bnj1190  29083  bnj1523  29146  atllat  29783

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938