Theorem simplbi 461

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 197	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 460	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  3simpa  1002  xoror  1408  sbequ2  1788  reurex  3045  eqimss  3516  pssss  3560  eldifi  3587  elinel1  3651  inss1  3682  ssunsn2  4156  pwssun  4756  sopo  4788  wefr  4840  opelxp1  4883  relop  5001  predel  5413  ordtr  5453  funmo  5614  funrel  5615  fnfun  5688  ffn  5743  f1f  5793  f1of1  5827  f1ofo  5835  isof1o  6228  eqopi  6838  1st2nd2  6841  reldmtpos  6986  swoer  7396  erdisj  7416  ecopover  7472  sdomdom  7601  mapfien  7924  inf3lemd  8135  cardprclem  8415  infxpenlem  8446  cardinfima  8529  dfac5lem4  8558  domtriomlem  8873  smobeth  9012  fpwwe2lem6  9061  fpwwe2lem7  9062  fpwwe2lem12  9067  fpwwe2lem13  9068  fpwwe2  9069  axrnegex  9587  axpre-sup  9594  zre  10942  nnssz  10958  ixxss1  11654  ixxss2  11655  ixxss12  11656  lbioo  11668  ubioo  11669  iccss2  11706  rge0ssre  11741  elfzuz  11797  uzdisj  11868  nn0disj  11908  0wrd0  12686  splfv1  12853  sqrlem6  13300  rlimf  13553  lo1f  13570  lo1dm  13571  o1f  13581  o1dm  13582  mertenslem2  13929  fprodge0  14035  divalglem9  14369  divalglem9OLD  14370  bitsinv2  14405  bitsf1ocnv  14406  gcdcllem1  14461  prmnn  14613  prmuz2  14630  coprmproddvdslem  14667  phimullem  14715  1arith  14859  ramtlecl  14939  0ramcl  14969  firest  15319  acsmre  15546  posprs  16182  latpos  16284  clatpos  16344  dlatl  16429  pslem  16440  tsrlemax  16454  tsrps  16455  sgrpmgm  16520  mndsgrp  16531  grpmnd  16666  nsgsubg  16837  ghmgrp1  16873  ghmgrp2  16874  gimghm  16916  gagrp  16934  gaset  16935  psgneu  17135  efgredeu  17390  ablgrp  17423  cmnmnd  17433  cyggenod2  17508  cyggrp  17512  ablfac2  17710  crngring  17779  dvdsrcl  17865  unitcl  17875  brric2  17961  drngring  17970  subrgring  17999  subrgrcl  18001  srngrhm  18067  lmimlmhm  18275  lveclmod  18317  2idlcpbl  18446  qus1  18447  qusrhm  18449  lpirring  18464  nzrring  18473  domnnzr  18507  fldidom  18517  assalmod  18531  assaring  18532  assasca  18533  cygznlem1  19124  cygznlem3  19127  lbslinds  19378  gsummatr01lem1  19667  topontop  19928  tpstop  19941  clsval2  20052  mretopd  20095  neiptoptop  20134  perftop  20159  restfpw  20182  cntop1  20243  cntop2  20244  cnptop1  20245  cnptop2  20246  cnprcl  20248  t1ficld  20330  t0top  20332  t1top  20333  haustop  20334  regtop  20336  nrmtop  20339  cnrmtop  20340  pnrmnrm  20343  cmptop  20397  discmp  20400  tgcmp  20403  uncmp  20405  conndisj  20418  contop  20419  1stctop  20445  llytop  20474  nllytop  20475  hmeocn  20762  filfbas  20850  ufilfil  20906  flimtop  20967  flimfil  20971  alexsublem  21046  ptcmplem3  21056  tsmsfbas  21129  tsmslem1  21130  tsmsgsum  21140  tsmssubm  21144  tsmsres  21145  tsmsf1o  21146  tsmsmhm  21147  tsmsadd  21148  tsmsxplem1  21154  tsmsxplem2  21155  tsmsxp  21156  tlmtmd  21188  tlmlmod  21190  tlmtrg  21191  tvctlm  21198  ressust  21266  uspreg  21276  ucncn  21287  neipcfilu  21298  cuspusp  21302  isxmet2d  21329  metxmet  21336  xmstps  21455  msxms  21456  xmsxmet  21458  msmet  21459  stdbdxmet  21517  nrgngp  21652  nlmngp  21667  nlmlmod  21668  nlmnrg  21669  nvcnlm  21685  nmoi  21720  nmoiOLD  21736  nghmrcl1  21740  nghmrcl2  21741  nmhmrcl1  21755  nmhmrcl2  21756  qdensere  21777  xrge0gsumle  21838  xrge0tsms  21839  metds0  21854  metdstri  21855  metdsre  21857  metdseq0  21858  metdscnlem  21859  metnrmlem1a  21862  metnrmlem1  21863  metds0OLD  21869  metdstriOLD  21870  metdsreOLD  21872  metdseq0OLD  21873  metdscnlemOLD  21874  metnrmlem1aOLD  21877  metnrmlem1OLD  21878  icopnfcnv  21957  cvsclm  22125  cmetmet  22243  cmsms  22303  hlbn  22317  ovolicc2lem5  22462  mblss  22472  mbff  22570  mbfres  22587  mbfadd  22604  mbfsub  22605  i1fmbf  22620  mbfmul  22671  bddmulibl  22783  limcmpt  22825  c1liplem1  22935  c1lip2  22937  fta1glem1  23103  fta1glem2  23104  fta1g  23105  fta1b  23107  ply1pid  23124  aacn  23257  ulmf2  23326  logdmnrp  23573  logdmss  23574  logcnlem2  23575  logcnlem3  23576  logcnlem4  23577  logcnlem5  23578  logcn  23579  dvloglem  23580  logf1o2  23582  efopnlem1  23588  logtayl2  23594  cxpcn  23672  cxpcn3lem  23674  cxpcn3  23675  resqrtcn  23676  atandmneg  23819  atandmcj  23822  cosatan  23834  cosatanne0  23835  birthdaylem1  23864  areacl  23875  cxp2lim  23889  jensenlem2  23900  jensen  23901  sqff1o  24096  dvdsmulf1o  24110  lgsqrlem1  24256  lgsqrlem2  24257  lgsqrlem3  24258  lgsqrlem4  24259  lgseisenlem3  24266  chebbnd1  24297  chtppilim  24300  chpchtlim  24304  chpo1ub  24305  dchrmusumlema  24318  dchrvmasumiflem1  24326  dchrisum0lema  24339  dchrisum0lem2  24343  selberg3lem2  24383  pntrsumo1  24390  selbergsb  24400  pnt2  24438  tglineeltr  24663  axcontlem2  24982  axcontlem7  24987  axcontlem8  24988  uhgra0v  25024  usgra0v  25085  usgra1v  25104  eupagra  25680  frgrawopreg  25763  ablogrpo  25998  smgrpismgmOLD  26046  mndoissmgrpOLD  26053  bnnv  26494  hlobn  26526  hcauseq  26824  hlimseqi  26828  hlimveci  26829  shss  26849  sh0  26855  chsh  26863  lnopf  27498  bdopln  27500  hmopf  27513  lnfnf  27523  unopf1o  27555  elunop2  27652  elpjhmop  27824  stcltrlem1  27915  mdslle1i  27956  mdslle2i  27957  rabexgfGS  28124  elin1d  28140  ssnnssfz  28361  tospos  28414  ogrpgrp  28461  ogrpinvOLD  28473  xrge0tsmsd  28544  ofldfld  28569  ofldlt1  28572  ofldchr  28573  isarchiofld  28576  reofld  28599  rearchi  28601  creftop  28669  lmxrge0  28754  qqhrhm  28789  esumpcvgval  28895  dynkin  28985  measssd  29033  elmbfmvol2  29085  omssubadd  29124  omssubaddOLD  29128  sibfinima  29168  eulerpartlemr  29203  eulerpartlemgf  29208  fiblem  29227  domprobmeas  29239  ballotlemscr  29347  ballotlemfg  29354  ballotlemfrc  29355  ballotlemfrceq  29357  ballotlemrinv0  29361  ballotlemscrOLD  29385  ballotlemfgOLD  29392  ballotlemfrcOLD  29393  ballotlemfrceqOLD  29395  ballotlemrinv0OLD  29399  bnj563  29549  bnj658  29557  bnj667  29558  bnj570  29712  bnj938  29744  bnj1001  29765  bnj1006  29766  bnj1049  29779  bnj1121  29790  bnj1173  29807  bnj1177  29811  bnj1245  29819  bnj1311  29829  bnj1321  29832  bnj1388  29838  bnj1398  29839  bnj1415  29843  bnj1417  29846  bnj1421  29847  bnj1442  29854  bnj1452  29857  bnj1489  29861  bnj1312  29863  pcontop  29944  sconpcon  29946  cvmcn  29981  cvmliftlem10  30013  fundmpss  30402  sltres  30546  funpartfun  30703  outsideofcol  30893  fnebas  30993  filnetlem3  31029  phpreu  31843  poimirlem26  31880  itg2addnc  31910  istotbnd3  32017  totbndmet  32018  sstotbnd2  32020  sstotbnd  32021  equivtotbnd  32024  bndmet  32027  totbndbnd  32035  prdstotbnd  32040  crngorngo  32147  prrngorngo  32198  divrngpr  32200  an3  32340  ollat  32698  omlol  32725  cvlatl  32810  hlomcmcv  32841  2dim  32954  1dimN  32955  lcfl8b  34991  lclkrlem2  35019  lclkrslem1  35024  lclkrslem2  35025  lcfrlem9  35037  mapdval2N  35117  mapdordlem2  35124  mapdrvallem2  35132  nacsacs  35470  eldiophelnn0  35525  lnmlmod  35857  lnrring  35891  mncply  35916  idomrootle  35989  idomodle  35990  hashgcdlem  35994  areaquad  36021  nznngen  36523  binomcxplemcvg  36561  2uasbanh  36786  fompt  37317  disjinfi  37318  stoweidlem14  37694  stoweidlem16  37696  stoweidlem24  37704  stoweidlem51  37732  stoweidlem54  37735  etransclem32  37951  sge0fodjrnlem  38046  ndmafv  38354  evenz  38471  oddz  38472  gbeeven  38567  gboodd  38568  uhgr0v  38827  usgr1vr  38925  uhg0v  38961  rnghmsubcsetclem1  39249  funcrngcsetcALT  39273  rhmsubcsetclem1  39295  rhmsubcrngclem1  39301  ssnn0ssfz  39404  elbigof  39639  digvalnn0  39684