Theorem simp1bi 996

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 194	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
3	2	simp1d 993	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ w3a 958

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960

This theorem is referenced by:  limord  4765  smores2  6801  smofvon2  6803  smofvon  6806  errel  7098  lincmb01cmp  11415  iccf1o  11416  elfznn0  11468  elfzouz  11541  ef01bndlem  13451  sin01bnd  13452  cos01bnd  13453  sin01gt0  13457  cos01gt0  13458  sin02gt0  13459  smueqlem  13669  gzcn  13976  mresspw  14513  drsprs  15089  ipodrscl  15315  subgrcl  15666  pmtrfconj  15952  pgpprm  16072  slwprm  16088  efgsdmi  16209  efgsrel  16211  efgs1b  16213  efgsp1  16214  efgsres  16215  efgsfo  16216  efgredlema  16217  efgredlemf  16218  efgredlemd  16221  efgredlemc  16222  efgredlem  16224  efgrelexlemb  16227  efgcpbllemb  16232  rnggrp  16586  irredcl  16730  lmodgrp  16879  lssss  16940  phllvec  17900  obsrcl  17990  fclstop  19426  tmdmnd  19488  tgpgrp  19491  trgtgp  19584  tdrgtrg  19589  ust0  19636  ngpgrp  20033  elii1  20349  elii2  20350  icopnfcnv  20356  icopnfhmeo  20357  iccpnfhmeo  20359  xrhmeo  20360  oprpiece1res1  20365  oprpiece1res2  20366  phtpcer  20409  pcoval2  20430  pcoass  20438  clmlmod  20481  cphphl  20532  cphnlm  20533  cphsca  20540  bnnvc  20693  uc1pcl  21500  mon1pcl  21501  sinq12ge0  21855  cosq14ge0  21858  cosord  21873  cos11  21874  recosf1o  21876  resinf1o  21877  efifo  21888  logrncn  21899  atanf  22160  atanneg  22187  efiatan  22192  atanlogaddlem  22193  atanlogadd  22194  atanlogsub  22196  efiatan2  22197  2efiatan  22198  tanatan  22199  areass  22238  dchrvmasumlem2  22632  dchrvmasumiflem1  22635  brbtwn2  22974  ax5seglem1  22997  ax5seglem2  22998  ax5seglem3  23000  ax5seglem5  23002  ax5seglem6  23003  ax5seglem9  23006  ax5seg  23007  axbtwnid  23008  axpaschlem  23009  axpasch  23010  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  subgores  23614  subgoid  23617  subgoinv  23618  sticl  25442  hstcl  25444  omndmnd  25991  srgcmn  26044  slmdcmn  26070  orngrng  26121  elunitrn  26181  rrextnrg  26284  rrextdrg  26285  eulerpartlemd  26597  eulerpartlemf  26601  eulerpartlemgvv  26607  eulerpartlemgu  26608  eulerpartlemgh  26609  eulerpartlemgs2  26611  eulerpartlemn  26612  locfintop  28416  stoweidlem60  29701  2spotiundisj  30501  bnj564  31459  bnj1366  31546  bnj545  31611  bnj548  31613  bnj558  31618  bnj570  31621  bnj580  31629  bnj929  31652  bnj998  31672  bnj1006  31675  bnj1190  31722  bnj1523  31785  atllat  32539