Theorem simplbi 462

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  3simpa  1004  xoror  1412  sbequ2  1798  reurex  3008  eqimss  3483  pssss  3527  eldifi  3554  elinel1  3618  elin1d  3621  inss1  3651  ssunsn2  4130  pwssun  4739  sopo  4771  wefr  4823  opelxp1  4866  relop  4984  predel  5396  ordtr  5436  funmo  5597  funrel  5598  fnfun  5671  ffn  5726  f1f  5777  f1of1  5811  f1ofo  5819  isof1o  6214  eqopi  6824  1st2nd2  6827  reldmtpos  6978  swoer  7388  erdisj  7408  ecopover  7464  sdomdom  7594  mapfien  7918  inf3lemd  8129  cardprclem  8410  infxpenlem  8441  cardinfima  8525  dfac5lem4  8554  domtriomlem  8869  smobeth  9008  fpwwe2lem6  9057  fpwwe2lem7  9058  fpwwe2lem12  9063  fpwwe2lem13  9064  fpwwe2  9065  axrnegex  9583  axpre-sup  9590  zre  10938  nnssz  10954  ixxss1  11650  ixxss2  11651  ixxss12  11652  lbioo  11664  ubioo  11665  iccss2  11702  rge0ssre  11737  elfzuz  11793  uzdisj  11864  nn0disj  11904  0wrd0  12690  splfv1  12857  sqrlem6  13304  rlimf  13558  lo1f  13575  lo1dm  13576  o1f  13586  o1dm  13587  mertenslem2  13934  fprodge0  14040  divalglem9  14374  divalglem9OLD  14375  bitsinv2  14410  bitsf1ocnv  14411  gcdcllem1  14466  prmnn  14618  prmuz2  14635  coprmproddvdslem  14672  phimullem  14720  1arith  14864  ramtlecl  14944  0ramcl  14974  firest  15324  acsmre  15551  posprs  16187  latpos  16289  clatpos  16349  dlatl  16434  pslem  16445  tsrlemax  16459  tsrps  16460  sgrpmgm  16525  mndsgrp  16536  grpmnd  16671  nsgsubg  16842  ghmgrp1  16878  ghmgrp2  16879  gimghm  16921  gagrp  16939  gaset  16940  psgneu  17140  efgredeu  17395  ablgrp  17428  cmnmnd  17438  cyggenod2  17513  cyggrp  17517  ablfac2  17715  crngring  17784  dvdsrcl  17870  unitcl  17880  brric2  17966  drngring  17975  subrgring  18004  subrgrcl  18006  srngrhm  18072  lmimlmhm  18280  lveclmod  18322  2idlcpbl  18451  qus1  18452  qusrhm  18454  lpirring  18469  nzrring  18478  domnnzr  18512  fldidom  18522  assalmod  18536  assaring  18537  assasca  18538  cygznlem1  19130  cygznlem3  19133  lbslinds  19384  gsummatr01lem1  19673  topontop  19934  tpstop  19947  clsval2  20058  mretopd  20101  neiptoptop  20140  perftop  20165  restfpw  20188  cntop1  20249  cntop2  20250  cnptop1  20251  cnptop2  20252  cnprcl  20254  t1ficld  20336  t0top  20338  t1top  20339  haustop  20340  regtop  20342  nrmtop  20345  cnrmtop  20346  pnrmnrm  20349  cmptop  20403  discmp  20406  tgcmp  20409  uncmp  20411  conndisj  20424  contop  20425  1stctop  20451  llytop  20480  nllytop  20481  hmeocn  20768  filfbas  20856  ufilfil  20912  flimtop  20973  flimfil  20977  alexsublem  21052  ptcmplem3  21062  tsmsfbas  21135  tsmslem1  21136  tsmsgsum  21146  tsmssubm  21150  tsmsres  21151  tsmsf1o  21152  tsmsmhm  21153  tsmsadd  21154  tsmsxplem1  21160  tsmsxplem2  21161  tsmsxp  21162  tlmtmd  21194  tlmlmod  21196  tlmtrg  21197  tvctlm  21204  ressust  21272  uspreg  21282  ucncn  21293  neipcfilu  21304  cuspusp  21308  isxmet2d  21335  metxmet  21342  xmstps  21461  msxms  21462  xmsxmet  21464  msmet  21465  stdbdxmet  21523  nrgngp  21658  nlmngp  21673  nlmlmod  21674  nlmnrg  21675  nvcnlm  21691  nmoi  21726  nmoiOLD  21742  nghmrcl1  21746  nghmrcl2  21747  nmhmrcl1  21761  nmhmrcl2  21762  qdensere  21783  xrge0gsumle  21844  xrge0tsms  21845  metds0  21860  metdstri  21861  metdsre  21863  metdseq0  21864  metdscnlem  21865  metnrmlem1a  21868  metnrmlem1  21869  metds0OLD  21875  metdstriOLD  21876  metdsreOLD  21878  metdseq0OLD  21879  metdscnlemOLD  21880  metnrmlem1aOLD  21883  metnrmlem1OLD  21884  icopnfcnv  21963  cvsclm  22131  cmetmet  22249  cmsms  22309  hlbn  22323  ovolicc2lem5  22468  mblss  22478  mbff  22576  mbfres  22593  mbfadd  22610  mbfsub  22611  i1fmbf  22626  mbfmul  22677  bddmulibl  22789  limcmpt  22831  c1liplem1  22941  c1lip2  22943  fta1glem1  23109  fta1glem2  23110  fta1g  23111  fta1b  23113  ply1pid  23130  aacn  23263  ulmf2  23332  logdmnrp  23579  logdmss  23580  logcnlem2  23581  logcnlem3  23582  logcnlem4  23583  logcnlem5  23584  logcn  23585  dvloglem  23586  logf1o2  23588  efopnlem1  23594  logtayl2  23600  cxpcn  23678  cxpcn3lem  23680  cxpcn3  23681  resqrtcn  23682  atandmneg  23825  atandmcj  23828  cosatan  23840  cosatanne0  23841  birthdaylem1  23870  areacl  23881  cxp2lim  23895  jensenlem2  23906  jensen  23907  sqff1o  24102  dvdsmulf1o  24116  lgsqrlem1  24262  lgsqrlem2  24263  lgsqrlem3  24264  lgsqrlem4  24265  lgseisenlem3  24272  chebbnd1  24303  chtppilim  24306  chpchtlim  24310  chpo1ub  24311  dchrmusumlema  24324  dchrvmasumiflem1  24332  dchrisum0lema  24345  dchrisum0lem2  24349  selberg3lem2  24389  pntrsumo1  24396  selbergsb  24406  pnt2  24444  tglineeltr  24669  axcontlem2  24988  axcontlem7  24993  axcontlem8  24994  uhgra0v  25030  usgra0v  25091  usgra1v  25110  eupagra  25687  frgrawopreg  25770  ablogrpo  26005  smgrpismgmOLD  26053  mndoissmgrpOLD  26060  bnnv  26501  hlobn  26533  hcauseq  26831  hlimseqi  26835  hlimveci  26836  shss  26856  sh0  26862  chsh  26870  lnopf  27505  bdopln  27507  hmopf  27520  lnfnf  27530  unopf1o  27562  elunop2  27659  elpjhmop  27831  stcltrlem1  27922  mdslle1i  27963  mdslle2i  27964  rabexgfGS  28130  ssnnssfz  28360  tospos  28412  ogrpgrp  28459  ogrpinvOLD  28471  xrge0tsmsd  28541  ofldfld  28566  ofldlt1  28569  ofldchr  28570  isarchiofld  28573  reofld  28596  rearchi  28598  creftop  28666  lmxrge0  28751  qqhrhm  28786  esumpcvgval  28892  dynkin  28982  measssd  29030  elmbfmvol2  29082  omssubadd  29121  omssubaddOLD  29125  sibfinima  29165  eulerpartlemr  29200  eulerpartlemgf  29205  fiblem  29224  domprobmeas  29236  ballotlemscr  29344  ballotlemfg  29351  ballotlemfrc  29352  ballotlemfrceq  29354  ballotlemrinv0  29358  ballotlemscrOLD  29382  ballotlemfgOLD  29389  ballotlemfrcOLD  29390  ballotlemfrceqOLD  29392  ballotlemrinv0OLD  29396  bnj563  29546  bnj658  29554  bnj667  29555  bnj570  29709  bnj938  29741  bnj1001  29762  bnj1006  29763  bnj1049  29776  bnj1121  29787  bnj1173  29804  bnj1177  29808  bnj1245  29816  bnj1311  29826  bnj1321  29829  bnj1388  29835  bnj1398  29836  bnj1415  29840  bnj1417  29843  bnj1421  29844  bnj1442  29851  bnj1452  29854  bnj1489  29858  bnj1312  29860  pcontop  29941  sconpcon  29943  cvmcn  29978  cvmliftlem10  30010  fundmpss  30400  sltres  30544  noseponlem  30548  funpartfun  30703  outsideofcol  30893  fnebas  30993  filnetlem3  31029  phpreu  31922  poimirlem26  31959  itg2addnc  31989  istotbnd3  32096  totbndmet  32097  sstotbnd2  32099  sstotbnd  32100  equivtotbnd  32103  bndmet  32106  totbndbnd  32114  prdstotbnd  32119  crngorngo  32226  prrngorngo  32277  divrngpr  32279  an3  32418  ollat  32773  omlol  32800  cvlatl  32885  hlomcmcv  32916  2dim  33029  1dimN  33030  lcfl8b  35066  lclkrlem2  35094  lclkrslem1  35099  lclkrslem2  35100  lcfrlem9  35112  mapdval2N  35192  mapdordlem2  35199  mapdrvallem2  35207  nacsacs  35545  eldiophelnn0  35600  lnmlmod  35931  lnrring  35965  mncply  35990  idomrootle  36063  idomodle  36064  hashgcdlem  36068  areaquad  36095  nznngen  36659  binomcxplemcvg  36697  2uasbanh  36922  fompt  37461  disjinfi  37462  stoweidlem14  37868  stoweidlem16  37870  stoweidlem24  37878  stoweidlem51  37906  stoweidlem54  37909  etransclem32  38125  sge0fodjrnlem  38252  ndmafv  38636  evenz  38753  oddz  38754  gbeeven  38849  gboodd  38850  ssrelrn  39006  uhgr0vb  39151  usgr1vr  39312  nbupgruvtxres  39463  cusgrusgr  39470  uhg0v  39676  rnghmsubcsetclem1  39964  funcrngcsetcALT  39988  rhmsubcsetclem1  40010  rhmsubcrngclem1  40016  ssnn0ssfz  40117  elbigof  40352  digvalnn0  40397