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  985  xoror  1358  sbequ2  1704  reurex  3041  eqimss  3515  pssss  3558  eldifi  3585  inss1  3677  ssunsn2  4139  pwssun  4734  sopo  4765  wefr  4817  ordtr  4840  opelxp1  4979  relop  5097  xpdifid  5373  funmo  5541  funrel  5542  fnfun  5615  ffn  5666  f1f  5713  f1of1  5747  f1ofo  5755  isof1o  6124  eqopi  6719  1st2nd2  6722  reldmtpos  6862  swoer  7238  erdisj  7257  ecopover  7313  sdomdom  7446  mapfien  7767  inf3lemd  7943  mapfienOLD  8037  cardprclem  8259  infxpenlem  8290  cardinfima  8377  dfac5lem4  8406  domtriomlem  8721  smobeth  8860  fpwwe2lem6  8912  fpwwe2lem7  8913  fpwwe2lem12  8918  fpwwe2lem13  8919  fpwwe2  8920  axrnegex  9439  axpre-sup  9446  zre  10760  nnssz  10776  ixxss1  11428  ixxss2  11429  ixxss12  11430  lbioo  11441  ubioo  11442  iccss2  11476  rge0ssre  11509  elfzuz  11565  uzdisj  11647  0wrd0  12370  splfv1  12514  sqrlem6  12854  rlimf  13096  lo1f  13113  lo1dm  13114  o1f  13124  o1dm  13125  fsumge0  13375  mertenslem2  13462  divalglem9  13722  bitsinv2  13756  bitsf1ocnv  13757  gcdcllem1  13812  prmnn  13883  prmind2  13891  nprm  13894  prmuz2  13898  isprm6  13912  exprmfct  13913  isprm5  13915  maxprmfct  13916  phibndlem  13962  phibnd  13963  dfphi2  13966  phimullem  13971  pclem  14022  pcprendvds2  14025  pcpre1  14026  expnprm  14081  prmreclem1  14094  1arith  14105  4sqlem15  14137  4sqlem16  14138  vdwlem5  14163  vdwlem6  14164  vdwlem8  14166  vdwlem9  14167  vdwlem11  14169  ramtlecl  14178  0ramcl  14201  firest  14489  acsmre  14708  posprs  15237  latpos  15338  clatpos  15398  dlatl  15483  pslem  15494  tsrlemax  15508  tsrps  15509  mndlem1  15537  grpmnd  15668  nsgsubg  15831  ghmgrp1  15867  ghmgrp2  15868  gimghm  15910  gagrp  15928  gaset  15929  psgneu  16130  efgredeu  16369  ablgrp  16402  cmnmnd  16412  cyggenod2  16482  cyggrp  16486  ablfac2  16711  crngrng  16777  dvdsrcl  16863  unitcl  16873  drngrng  16961  subrgrng  16990  subrgrcl  16992  srngrhm  17058  lmimlmhm  17267  lveclmod  17309  2idlcpbl  17438  divs1  17439  divsrhm  17441  lpirrng  17456  nzrrng  17465  domnnzr  17489  fldidom  17499  assalmod  17513  assarng  17514  assasca  17515  cygznlem1  18123  cygznlem3  18126  lbslinds  18386  gsummatr01lem1  18592  topontop  18662  tpstop  18675  clsval2  18785  mretopd  18827  neiptoptop  18866  perftop  18891  restfpw  18914  cntop1  18975  cntop2  18976  cnptop1  18977  cnptop2  18978  cnprcl  18980  t1ficld  19062  t0top  19064  t1top  19065  haustop  19066  regtop  19068  nrmtop  19071  cnrmtop  19072  pnrmnrm  19075  cmptop  19129  discmp  19132  tgcmp  19135  uncmp  19137  conndisj  19151  contop  19152  1stctop  19178  llytop  19207  nllytop  19208  hmeocn  19464  filfbas  19552  ufilfil  19608  flimtop  19669  flimfil  19673  alexsublem  19747  ptcmplem3  19757  tsmsfbas  19829  tsmslem1  19830  tsmsgsum  19840  tsmsgsumOLD  19843  tsmssubm  19847  tsmsresOLD  19848  tsmsres  19849  tsmsf1o  19850  tsmsmhm  19851  tsmsadd  19852  tsmsxplem1  19858  tsmsxplem2  19859  tsmsxp  19860  tlmtmd  19892  tlmlmod  19894  tlmtrg  19895  tvctlm  19902  ressust  19970  uspreg  19980  ucncn  19991  neipcfilu  20002  cuspusp  20006  isxmet2d  20033  metxmet  20040  xmstps  20159  msxms  20160  xmsxmet  20162  msmet  20163  stdbdxmet  20221  nrgngp  20374  nlmngp  20389  nlmlmod  20390  nlmnrg  20391  nvcnlm  20407  nmoi  20438  nghmrcl1  20442  nghmrcl2  20443  nmhmrcl1  20457  nmhmrcl2  20458  qdensere  20480  xrge0gsumle  20541  xrge0tsms  20542  metds0  20557  metdstri  20558  metdsre  20560  metdseq0  20561  metdscnlem  20562  metnrmlem1a  20565  metnrmlem1  20566  icopnfcnv  20645  icopnfhmeo  20646  cvsclm  20810  cmetmet  20928  cmsms  20990  hlbn  21006  ovolicc1  21130  ovolicc2lem5  21135  mblss  21145  mbff  21237  mbfres  21254  mbfadd  21271  mbfsub  21272  i1fmbf  21285  mbfmul  21336  bddmulibl  21448  limcmpt  21490  c1liplem1  21600  c1lip2  21602  fta1glem1  21769  fta1glem2  21770  fta1g  21771  fta1b  21773  ply1pid  21783  aacn  21915  ulmf2  21981  logdmnrp  22218  logdmss  22219  logcnlem2  22220  logcnlem3  22221  logcnlem4  22222  logcnlem5  22223  logcn  22224  dvloglem  22225  logf1o2  22227  efopnlem1  22233  logtayl2  22239  cxpcn  22315  cxpcn3lem  22317  cxpcn3  22318  resqrcn  22319  atandmneg  22433  atandmcj  22436  cosatan  22448  cosatanne0  22449  birthdaylem1  22477  areacl  22488  cxp2lim  22502  jensenlem2  22513  jensen  22514  wilth  22541  sqff1o  22652  dvdsmulf1o  22666  mersenne  22698  bposlem3  22757  lgsqrlem1  22812  lgsqrlem2  22813  lgsqrlem3  22814  lgsqrlem4  22815  lgseisenlem3  22822  lgsquad2lem2  22830  2sqlem6  22840  chebbnd1  22853  chtppilim  22856  chpchtlim  22860  chpo1ub  22861  rplogsumlem1  22865  rplogsumlem2  22866  dchrmusumlema  22874  dchrvmasumiflem1  22882  dchrisum0flblem2  22890  dchrisum0lema  22895  dchrisum0lem2  22899  selberg3lem2  22939  pntrsumo1  22946  selbergsb  22956  pnt2  22994  ostthlem2  23009  ostth2lem2  23015  tglineeltr  23175  axcontlem2  23362  axcontlem7  23367  axcontlem8  23368  axcontlem10  23370  uhgra0v  23395  usgra0v  23441  usgra1v  23459  eupagra  23738  ablogrpo  23922  smgrpismgm  23970  mndoissmgrp  23977  nmogtmnf  24321  bnnv  24418  hlobn  24440  hcauseq  24738  hlimseqi  24742  hlimveci  24743  shss  24763  sh0  24769  chsh  24778  lnopf  25414  bdopln  25416  nmopgtmnf  25423  hmopf  25429  lnfnf  25439  unopf1o  25471  elunop2  25568  elpjhmop  25740  stcltrlem1  25831  mdslle1i  25872  mdslle2i  25873  rabexgfGS  26037  suppss3  26177  ssnnssfz  26220  tospos  26263  ogrpgrp  26310  ogrpinvOLD  26322  ogrpinv0le  26323  ogrpsub  26324  ogrpaddlt  26325  archirng  26349  archirngz  26350  archiabllem1a  26352  archiabllem1b  26353  archiabllem1  26354  archiabllem2a  26355  archiabllem2c  26356  archiabllem2b  26357  archiabllem2  26358  xrge0tsmsd  26397  ofldfld  26422  ofldlt1  26425  ofldchr  26426  isarchiofld  26429  reofld  26452  rearchi  26454  lmxrge0  26526  qqhrhm  26562  esumpcvgval  26671  measssd  26773  elmbfmvol2  26825  sibfinima  26868  eulerpartlemr  26900  eulerpartlemgf  26905  fiblem  26924  domprobmeas  26936  ballotlemscr  27044  ballotlemfg  27051  ballotlemfrc  27052  ballotlemfrceq  27054  ballotlemrinv0  27058  signstfveq0  27121  subfacval3  27220  pcontop  27257  sconpcon  27259  cvmcn  27294  cvmliftlem10  27326  fundmpss  27720  predel  27787  sltres  27948  funpartfun  28117  outsideofcol  28307  itg2addnc  28593  itg2gt0cn  28594  ftc1anclem3  28616  fnebas  28692  filnetlem3  28748  istotbnd3  28817  totbndmet  28818  sstotbnd2  28820  sstotbnd  28821  equivtotbnd  28824  bndmet  28827  totbndbnd  28835  prdstotbnd  28840  crngorngo  28947  prrngorngo  28998  divrngpr  29000  an3  29142  nacsacs  29192  eldiophelnn0  29249  jm2.17a  29450  jm2.17b  29451  jm2.17c  29452  jm2.27c  29503  jm3.1lem1  29513  jm3.1lem2  29514  jm3.1lem3  29515  lnmlmod  29579  lnrrng  29615  mncply  29641  idomrootle  29707  idomodle  29708  hashgcdlem  29712  areaquad  29739  stoweidlem14  29956  stoweidlem16  29958  stoweidlem24  29966  stoweidlem39  29981  stoweidlem50  29992  stoweidlem51  29993  stoweidlem54  29996  stoweidlem57  29999  wallispilem3  30009  ndmafv  30193  rusgranumwlks  30721  frgrawopreg  30789  nn0disj  30885  ssnn0ssfz  30888  2uasbanh  31587  bnj563  32052  bnj658  32060  bnj667  32061  bnj570  32215  bnj938  32247  bnj1001  32268  bnj1006  32269  bnj1049  32282  bnj1121  32293  bnj1173  32310  bnj1177  32314  bnj1245  32322  bnj1311  32332  bnj1321  32335  bnj1388  32341  bnj1398  32342  bnj1415  32346  bnj1417  32349  bnj1421  32350  bnj1442  32357  bnj1452  32360  bnj1489  32364  bnj1312  32366  ollat  33181  omlol  33208  cvlatl  33293  hlomcmcv  33324  2dim  33437  1dimN  33438  lcfl8b  35472  lclkrlem2  35500  lclkrslem1  35505  lclkrslem2  35506  lcfrlem9  35518  mapdval2N  35598  mapdordlem2  35605  mapdrvallem2  35613