Theorem simplbi 460

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simplbi	|- ( ph -> ps )

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 194	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 459	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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

This theorem is referenced by:  3simpa  993  xoror  1370  sbequ2  1742  reurex  3074  eqimss  3551  pssss  3595  eldifi  3622  inss1  3714  ssunsn2  4191  pwssun  4795  sopo  4826  wefr  4878  ordtr  4901  opelxp1  5041  relop  5163  funmo  5610  funrel  5611  fnfun  5684  ffn  5737  f1f  5787  f1of1  5821  f1ofo  5829  isof1o  6222  eqopi  6833  1st2nd2  6836  reldmtpos  6981  swoer  7357  erdisj  7377  ecopover  7433  sdomdom  7562  mapfien  7885  inf3lemd  8061  mapfienOLD  8155  cardprclem  8377  infxpenlem  8408  cardinfima  8495  dfac5lem4  8524  domtriomlem  8839  smobeth  8978  fpwwe2lem6  9030  fpwwe2lem7  9031  fpwwe2lem12  9036  fpwwe2lem13  9037  fpwwe2  9038  axrnegex  9556  axpre-sup  9563  zre  10889  nnssz  10905  ixxss1  11572  ixxss2  11573  ixxss12  11574  lbioo  11585  ubioo  11586  iccss2  11620  rge0ssre  11653  elfzuz  11709  uzdisj  11777  nn0disj  11817  0wrd0  12575  splfv1  12743  sqrlem6  13093  rlimf  13336  lo1f  13353  lo1dm  13354  o1f  13364  o1dm  13365  mertenslem2  13706  divalglem9  14071  bitsinv2  14105  bitsf1ocnv  14106  gcdcllem1  14161  prmnn  14232  prmuz2  14247  phimullem  14321  1arith  14457  ramtlecl  14530  0ramcl  14553  firest  14850  acsmre  15069  posprs  15705  latpos  15807  clatpos  15867  dlatl  15952  pslem  15963  tsrlemax  15977  tsrps  15978  sgrpmgm  16043  mndsgrp  16054  grpmnd  16189  nsgsubg  16360  ghmgrp1  16396  ghmgrp2  16397  gimghm  16439  gagrp  16457  gaset  16458  psgneu  16658  efgredeu  16897  ablgrp  16930  cmnmnd  16940  cyggenod2  17015  cyggrp  17019  ablfac2  17267  crngring  17336  dvdsrcl  17425  unitcl  17435  brric2  17521  drngring  17530  subrgring  17559  subrgrcl  17561  srngrhm  17627  lmimlmhm  17837  lveclmod  17879  2idlcpbl  18009  qus1  18010  qusrhm  18012  lpirring  18027  nzrring  18036  domnnzr  18071  fldidom  18081  assalmod  18095  assaring  18096  assasca  18097  cygznlem1  18732  cygznlem3  18735  lbslinds  18995  gsummatr01lem1  19284  topontop  19554  tpstop  19567  clsval2  19678  mretopd  19720  neiptoptop  19759  perftop  19784  restfpw  19807  cntop1  19868  cntop2  19869  cnptop1  19870  cnptop2  19871  cnprcl  19873  t1ficld  19955  t0top  19957  t1top  19958  haustop  19959  regtop  19961  nrmtop  19964  cnrmtop  19965  pnrmnrm  19968  cmptop  20022  discmp  20025  tgcmp  20028  uncmp  20030  conndisj  20043  contop  20044  1stctop  20070  llytop  20099  nllytop  20100  hmeocn  20387  filfbas  20475  ufilfil  20531  flimtop  20592  flimfil  20596  alexsublem  20670  ptcmplem3  20680  tsmsfbas  20752  tsmslem1  20753  tsmsgsum  20763  tsmsgsumOLD  20766  tsmssubm  20770  tsmsresOLD  20771  tsmsres  20772  tsmsf1o  20773  tsmsmhm  20774  tsmsadd  20775  tsmsxplem1  20781  tsmsxplem2  20782  tsmsxp  20783  tlmtmd  20815  tlmlmod  20817  tlmtrg  20818  tvctlm  20825  ressust  20893  uspreg  20903  ucncn  20914  neipcfilu  20925  cuspusp  20929  isxmet2d  20956  metxmet  20963  xmstps  21082  msxms  21083  xmsxmet  21085  msmet  21086  stdbdxmet  21144  nrgngp  21297  nlmngp  21312  nlmlmod  21313  nlmnrg  21314  nvcnlm  21330  nmoi  21361  nghmrcl1  21365  nghmrcl2  21366  nmhmrcl1  21380  nmhmrcl2  21381  qdensere  21403  xrge0gsumle  21464  xrge0tsms  21465  metds0  21480  metdstri  21481  metdsre  21483  metdseq0  21484  metdscnlem  21485  metnrmlem1a  21488  metnrmlem1  21489  icopnfcnv  21568  cvsclm  21733  cmetmet  21851  cmsms  21913  hlbn  21929  ovolicc2lem5  22058  mblss  22068  mbff  22160  mbfres  22177  mbfadd  22194  mbfsub  22195  i1fmbf  22208  mbfmul  22259  bddmulibl  22371  limcmpt  22413  c1liplem1  22523  c1lip2  22525  fta1glem1  22692  fta1glem2  22693  fta1g  22694  fta1b  22696  ply1pid  22706  aacn  22839  ulmf2  22905  logdmnrp  23148  logdmss  23149  logcnlem2  23150  logcnlem3  23151  logcnlem4  23152  logcnlem5  23153  logcn  23154  dvloglem  23155  logf1o2  23157  efopnlem1  23163  logtayl2  23169  cxpcn  23245  cxpcn3lem  23247  cxpcn3  23248  resqrtcn  23249  atandmneg  23363  atandmcj  23366  cosatan  23378  cosatanne0  23379  birthdaylem1  23407  areacl  23418  cxp2lim  23432  jensenlem2  23443  jensen  23444  sqff1o  23582  dvdsmulf1o  23596  lgsqrlem1  23742  lgsqrlem2  23743  lgsqrlem3  23744  lgsqrlem4  23745  lgseisenlem3  23752  chebbnd1  23783  chtppilim  23786  chpchtlim  23790  chpo1ub  23791  dchrmusumlema  23804  dchrvmasumiflem1  23812  dchrisum0lema  23825  dchrisum0lem2  23829  selberg3lem2  23869  pntrsumo1  23876  selbergsb  23886  pnt2  23924  tglineeltr  24137  axcontlem2  24395  axcontlem7  24400  axcontlem8  24401  uhgra0v  24437  usgra0v  24498  usgra1v  24517  eupagra  25093  frgrawopreg  25176  ablogrpo  25413  smgrpismgmOLD  25461  mndoissmgrpOLD  25468  bnnv  25909  hlobn  25931  hcauseq  26229  hlimseqi  26233  hlimveci  26234  shss  26254  sh0  26260  chsh  26269  lnopf  26905  bdopln  26907  hmopf  26920  lnfnf  26930  unopf1o  26962  elunop2  27059  elpjhmop  27231  stcltrlem1  27322  mdslle1i  27363  mdslle2i  27364  rabexgfGS  27529  elin1d  27546  ssnnssfz  27757  tospos  27806  ogrpgrp  27853  ogrpinvOLD  27865  xrge0tsmsd  27936  ofldfld  27961  ofldlt1  27964  ofldchr  27965  isarchiofld  27968  reofld  27991  rearchi  27993  creftop  28010  lmxrge0  28095  qqhrhm  28131  esumpcvgval  28250  measssd  28359  elmbfmvol2  28411  omssubadd  28444  sibfinima  28478  eulerpartlemr  28510  eulerpartlemgf  28515  fiblem  28534  domprobmeas  28546  ballotlemscr  28654  ballotlemfg  28661  ballotlemfrc  28662  ballotlemfrceq  28664  ballotlemrinv0  28668  pcontop  28867  sconpcon  28869  cvmcn  28904  cvmliftlem10  28936  fundmpss  29393  predel  29459  sltres  29620  funpartfun  29777  outsideofcol  29967  itg2addnc  30253  fnebas  30346  filnetlem3  30382  istotbnd3  30451  totbndmet  30452  sstotbnd2  30454  sstotbnd  30455  equivtotbnd  30458  bndmet  30461  totbndbnd  30469  prdstotbnd  30474  crngorngo  30581  prrngorngo  30632  divrngpr  30634  an3  30775  nacsacs  30825  eldiophelnn0  30881  lnmlmod  31208  lnrring  31244  mncply  31269  idomrootle  31335  idomodle  31336  hashgcdlem  31340  areaquad  31367  nznngen  31404  binomcxplemcvg  31442  elinel1  31606  fprodge0  31779  stoweidlem14  31978  stoweidlem16  31980  stoweidlem24  31988  stoweidlem51  32015  stoweidlem54  32018  etransclem32  32231  ndmafv  32407  uhg0v  32618  rnghmsubcsetclem1  32906  funcrngcsetcALT  32930  rhmsubcsetclem1  32952  rhmsubcrngclem1  32958  ssnn0ssfz  33061  2uasbanh  33456  bnj563  33922  bnj658  33930  bnj667  33931  bnj570  34085  bnj938  34117  bnj1001  34138  bnj1006  34139  bnj1049  34152  bnj1121  34163  bnj1173  34180  bnj1177  34184  bnj1245  34192  bnj1311  34202  bnj1321  34205  bnj1388  34211  bnj1398  34212  bnj1415  34216  bnj1417  34219  bnj1421  34220  bnj1442  34227  bnj1452  34230  bnj1489  34234  bnj1312  34236  ollat  35060  omlol  35087  cvlatl  35172  hlomcmcv  35203  2dim  35316  1dimN  35317  lcfl8b  37353  lclkrlem2  37381  lclkrslem1  37386  lclkrslem2  37387  lcfrlem9  37399  mapdval2N  37479  mapdordlem2  37486  mapdrvallem2  37494