Theorem simplbi 458

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

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

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 369

This theorem is referenced by:  3simpa  994  xoror  1374  sbequ2  1765  reurex  3024  eqimss  3494  pssss  3538  eldifi  3565  elinel1  3628  inss1  3659  ssunsn2  4131  pwssun  4729  sopo  4761  wefr  4813  opelxp1  4856  relop  4974  predel  5384  ordtr  5424  funmo  5585  funrel  5586  fnfun  5659  ffn  5714  f1f  5764  f1of1  5798  f1ofo  5806  isof1o  6204  eqopi  6818  1st2nd2  6821  reldmtpos  6966  swoer  7376  erdisj  7396  ecopover  7452  sdomdom  7581  mapfien  7901  inf3lemd  8077  mapfienOLD  8170  cardprclem  8392  infxpenlem  8423  cardinfima  8510  dfac5lem4  8539  domtriomlem  8854  smobeth  8993  fpwwe2lem6  9043  fpwwe2lem7  9044  fpwwe2lem12  9049  fpwwe2lem13  9050  fpwwe2  9051  axrnegex  9569  axpre-sup  9576  zre  10909  nnssz  10925  ixxss1  11600  ixxss2  11601  ixxss12  11602  lbioo  11613  ubioo  11614  iccss2  11649  rge0ssre  11682  elfzuz  11738  uzdisj  11806  nn0disj  11846  0wrd0  12620  splfv1  12787  sqrlem6  13230  rlimf  13473  lo1f  13490  lo1dm  13491  o1f  13501  o1dm  13502  mertenslem2  13846  divalglem9  14268  bitsinv2  14302  bitsf1ocnv  14303  gcdcllem1  14358  prmnn  14429  prmuz2  14444  phimullem  14518  1arith  14654  ramtlecl  14727  0ramcl  14750  firest  15047  acsmre  15266  posprs  15902  latpos  16004  clatpos  16064  dlatl  16149  pslem  16160  tsrlemax  16174  tsrps  16175  sgrpmgm  16240  mndsgrp  16251  grpmnd  16386  nsgsubg  16557  ghmgrp1  16593  ghmgrp2  16594  gimghm  16636  gagrp  16654  gaset  16655  psgneu  16855  efgredeu  17094  ablgrp  17127  cmnmnd  17137  cyggenod2  17212  cyggrp  17216  ablfac2  17460  crngring  17529  dvdsrcl  17618  unitcl  17628  brric2  17714  drngring  17723  subrgring  17752  subrgrcl  17754  srngrhm  17820  lmimlmhm  18030  lveclmod  18072  2idlcpbl  18202  qus1  18203  qusrhm  18205  lpirring  18220  nzrring  18229  domnnzr  18264  fldidom  18274  assalmod  18288  assaring  18289  assasca  18290  cygznlem1  18903  cygznlem3  18906  lbslinds  19160  gsummatr01lem1  19449  topontop  19719  tpstop  19732  clsval2  19843  mretopd  19886  neiptoptop  19925  perftop  19950  restfpw  19973  cntop1  20034  cntop2  20035  cnptop1  20036  cnptop2  20037  cnprcl  20039  t1ficld  20121  t0top  20123  t1top  20124  haustop  20125  regtop  20127  nrmtop  20130  cnrmtop  20131  pnrmnrm  20134  cmptop  20188  discmp  20191  tgcmp  20194  uncmp  20196  conndisj  20209  contop  20210  1stctop  20236  llytop  20265  nllytop  20266  hmeocn  20553  filfbas  20641  ufilfil  20697  flimtop  20758  flimfil  20762  alexsublem  20836  ptcmplem3  20846  tsmsfbas  20918  tsmslem1  20919  tsmsgsum  20929  tsmsgsumOLD  20932  tsmssubm  20936  tsmsresOLD  20937  tsmsres  20938  tsmsf1o  20939  tsmsmhm  20940  tsmsadd  20941  tsmsxplem1  20947  tsmsxplem2  20948  tsmsxp  20949  tlmtmd  20981  tlmlmod  20983  tlmtrg  20984  tvctlm  20991  ressust  21059  uspreg  21069  ucncn  21080  neipcfilu  21091  cuspusp  21095  isxmet2d  21122  metxmet  21129  xmstps  21248  msxms  21249  xmsxmet  21251  msmet  21252  stdbdxmet  21310  nrgngp  21463  nlmngp  21478  nlmlmod  21479  nlmnrg  21480  nvcnlm  21496  nmoi  21527  nghmrcl1  21531  nghmrcl2  21532  nmhmrcl1  21546  nmhmrcl2  21547  qdensere  21569  xrge0gsumle  21630  xrge0tsms  21631  metds0  21646  metdstri  21647  metdsre  21649  metdseq0  21650  metdscnlem  21651  metnrmlem1a  21654  metnrmlem1  21655  icopnfcnv  21734  cvsclm  21899  cmetmet  22017  cmsms  22079  hlbn  22095  ovolicc2lem5  22224  mblss  22234  mbff  22326  mbfres  22343  mbfadd  22360  mbfsub  22361  i1fmbf  22374  mbfmul  22425  bddmulibl  22537  limcmpt  22579  c1liplem1  22689  c1lip2  22691  fta1glem1  22858  fta1glem2  22859  fta1g  22860  fta1b  22862  ply1pid  22872  aacn  23005  ulmf2  23071  logdmnrp  23316  logdmss  23317  logcnlem2  23318  logcnlem3  23319  logcnlem4  23320  logcnlem5  23321  logcn  23322  dvloglem  23323  logf1o2  23325  efopnlem1  23331  logtayl2  23337  cxpcn  23415  cxpcn3lem  23417  cxpcn3  23418  resqrtcn  23419  atandmneg  23562  atandmcj  23565  cosatan  23577  cosatanne0  23578  birthdaylem1  23607  areacl  23618  cxp2lim  23632  jensenlem2  23643  jensen  23644  sqff1o  23837  dvdsmulf1o  23851  lgsqrlem1  23997  lgsqrlem2  23998  lgsqrlem3  23999  lgsqrlem4  24000  lgseisenlem3  24007  chebbnd1  24038  chtppilim  24041  chpchtlim  24045  chpo1ub  24046  dchrmusumlema  24059  dchrvmasumiflem1  24067  dchrisum0lema  24080  dchrisum0lem2  24084  selberg3lem2  24124  pntrsumo1  24131  selbergsb  24141  pnt2  24179  tglineeltr  24396  axcontlem2  24685  axcontlem7  24690  axcontlem8  24691  uhgra0v  24727  usgra0v  24788  usgra1v  24807  eupagra  25383  frgrawopreg  25466  ablogrpo  25700  smgrpismgmOLD  25748  mndoissmgrpOLD  25755  bnnv  26196  hlobn  26218  hcauseq  26516  hlimseqi  26520  hlimveci  26521  shss  26541  sh0  26547  chsh  26556  lnopf  27191  bdopln  27193  hmopf  27206  lnfnf  27216  unopf1o  27248  elunop2  27345  elpjhmop  27517  stcltrlem1  27608  mdslle1i  27649  mdslle2i  27650  rabexgfGS  27816  elin1d  27832  ssnnssfz  28045  tospos  28098  ogrpgrp  28145  ogrpinvOLD  28157  xrge0tsmsd  28228  ofldfld  28253  ofldlt1  28256  ofldchr  28257  isarchiofld  28260  reofld  28283  rearchi  28285  creftop  28302  lmxrge0  28387  qqhrhm  28422  esumpcvgval  28525  dynkin  28615  measssd  28663  elmbfmvol2  28715  omssubadd  28748  sibfinima  28787  eulerpartlemr  28819  eulerpartlemgf  28824  fiblem  28843  domprobmeas  28855  ballotlemscr  28963  ballotlemfg  28970  ballotlemfrc  28971  ballotlemfrceq  28973  ballotlemrinv0  28977  bnj563  29127  bnj658  29135  bnj667  29136  bnj570  29290  bnj938  29322  bnj1001  29343  bnj1006  29344  bnj1049  29357  bnj1121  29368  bnj1173  29385  bnj1177  29389  bnj1245  29397  bnj1311  29407  bnj1321  29410  bnj1388  29416  bnj1398  29417  bnj1415  29421  bnj1417  29424  bnj1421  29425  bnj1442  29432  bnj1452  29435  bnj1489  29439  bnj1312  29441  pcontop  29522  sconpcon  29524  cvmcn  29559  cvmliftlem10  29591  fundmpss  29980  sltres  30124  funpartfun  30281  outsideofcol  30471  fnebas  30572  filnetlem3  30608  itg2addnc  31442  istotbnd3  31549  totbndmet  31550  sstotbnd2  31552  sstotbnd  31553  equivtotbnd  31556  bndmet  31559  totbndbnd  31567  prdstotbnd  31572  crngorngo  31679  prrngorngo  31730  divrngpr  31732  an3  31873  ollat  32231  omlol  32258  cvlatl  32343  hlomcmcv  32374  2dim  32487  1dimN  32488  lcfl8b  34524  lclkrlem2  34552  lclkrslem1  34557  lclkrslem2  34558  lcfrlem9  34570  mapdval2N  34650  mapdordlem2  34657  mapdrvallem2  34665  nacsacs  35003  eldiophelnn0  35058  lnmlmod  35387  lnrring  35425  mncply  35450  idomrootle  35516  idomodle  35517  hashgcdlem  35521  areaquad  35548  nznngen  36069  binomcxplemcvg  36107  2uasbanh  36358  fprodge0  36965  stoweidlem14  37164  stoweidlem16  37166  stoweidlem24  37174  stoweidlem51  37201  stoweidlem54  37204  etransclem32  37417  ndmafv  37593  evenz  37712  oddz  37713  gbeeven  37808  gboodd  37809  uhg0v  38006  rnghmsubcsetclem1  38294  funcrngcsetcALT  38318  rhmsubcsetclem1  38340  rhmsubcrngclem1  38346  ssnn0ssfz  38449  elbigof  38685  digvalnn0  38730