Theorem simplbi 447

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  3simpa  954  sbequ2  1657  reurex  2882  eqimss  3360  pssss  3402  eldifi  3429  inss1  3521  ssunsn2  3918  pwssun  4449  sopo  4480  wefr  4532  ordtr  4555  opelxp1  4870  relop  4982  funmo  5429  funrel  5430  fnfun  5501  ffn  5550  f1f  5598  f1of1  5632  f1ofo  5640  isof1o  6004  eqopi  6342  1st2nd2  6345  reldmtpos  6446  swoer  6892  erdisj  6911  ecopover  6967  sdomdom  7094  inf3lemd  7538  mapfien  7609  cardprclem  7822  infxpenlem  7851  cardinfima  7934  dfac5lem4  7963  domtriomlem  8278  smobeth  8417  fpwwe2lem6  8466  fpwwe2lem7  8467  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  axrnegex  8993  axpre-sup  9000  zre  10242  nnssz  10257  ixxss1  10890  ixxss2  10891  ixxss12  10892  lbioo  10903  ubioo  10904  iccss2  10937  elfzuz  11011  uzdisj  11074  splfv1  11739  sqrlem6  12008  rlimf  12250  lo1f  12267  lo1dm  12268  o1f  12278  o1dm  12279  fsumge0  12529  mertenslem2  12617  divalglem9  12876  bitsinv2  12910  bitsf1ocnv  12911  gcdcllem1  12966  prmnn  13037  prmind2  13045  nprm  13048  prmuz2  13052  isprm6  13064  exprmfct  13065  isprm5  13067  maxprmfct  13068  phibndlem  13114  phibnd  13115  dfphi2  13118  phimullem  13123  pclem  13167  pcprendvds2  13170  pcpre1  13171  expnprm  13226  prmreclem1  13239  1arith  13250  4sqlem15  13282  4sqlem16  13283  vdwlem5  13308  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  vdwlem11  13314  ramtlecl  13323  0ramcl  13346  firest  13615  acsmre  13832  posprs  14361  latpos  14433  dlatl  14576  pslem  14593  tsrlemax  14607  tsrps  14608  laps  14623  mndlem1  14649  grpmnd  14772  nsgsubg  14927  ghmgrp1  14963  ghmgrp2  14964  gimghm  15006  gagrp  15024  gaset  15025  efgredeu  15339  ablgrp  15372  cmnmnd  15382  cyggenod2  15450  cyggrp  15454  ablfac2  15602  crngrng  15629  dvdsrcl  15709  unitcl  15719  drngrng  15797  subrgrng  15826  subrgrcl  15828  srngrhm  15894  lmimlmhm  16091  lveclmod  16133  2idlcpbl  16260  divs1  16261  divsrhm  16263  lpirrng  16278  nzrrng  16287  domnnzr  16310  fldidom  16320  assalmod  16334  assarng  16335  assasca  16336  cygznlem1  16802  cygznlem3  16805  topontop  16946  tpstop  16959  clsval2  17069  mretopd  17111  neiptoptop  17150  perftop  17174  restfpw  17197  cntop1  17258  cntop2  17259  cnptop1  17260  cnptop2  17261  cnprcl  17263  t1ficld  17345  t0top  17347  t1top  17348  haustop  17349  regtop  17351  nrmtop  17354  cnrmtop  17355  pnrmnrm  17358  cmptop  17412  discmp  17415  tgcmp  17418  uncmp  17420  conndisj  17432  contop  17433  1stctop  17459  llytop  17488  nllytop  17489  hmeocn  17745  filfbas  17833  ufilfil  17889  flimtop  17950  flimfil  17954  alexsublem  18028  ptcmplem3  18038  tsmsfbas  18110  tsmslem1  18111  tsmsgsum  18121  tsmssubm  18125  tsmsres  18126  tsmsf1o  18127  tsmsmhm  18128  tsmsadd  18129  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  tlmtmd  18169  tlmlmod  18171  tlmtrg  18172  tvctlm  18179  ressust  18247  uspreg  18257  ucncn  18268  neipcfilu  18279  cuspusp  18283  isxmet2d  18310  metxmet  18317  xmstps  18436  msxms  18437  xmsxmet  18439  msmet  18440  stdbdxmet  18498  nrgngp  18651  nlmngp  18666  nlmlmod  18667  nlmnrg  18668  nvcnlm  18684  nmoi  18715  nghmrcl1  18719  nghmrcl2  18720  nmhmrcl1  18734  nmhmrcl2  18735  qdensere  18757  xrge0gsumle  18817  xrge0tsms  18818  metds0  18833  metdstri  18834  metdsre  18836  metdseq0  18837  metdscnlem  18838  metnrmlem1a  18841  metnrmlem1  18842  icopnfcnv  18920  icopnfhmeo  18921  cmetmet  19192  cmsms  19254  hlbn  19270  ovolicc1  19365  ovolicc2lem5  19370  mblss  19380  mbff  19472  mbfres  19489  mbfadd  19506  mbfsub  19507  i1fmbf  19520  mbfmul  19571  bddmulibl  19683  limcmpt  19723  c1liplem1  19833  c1lip2  19835  fta1glem1  20041  fta1glem2  20042  fta1g  20043  fta1b  20045  ply1pid  20055  aacn  20187  ulmf2  20253  logdmnrp  20485  logdmss  20486  logcnlem2  20487  logcnlem3  20488  logcnlem4  20489  logcnlem5  20490  logcn  20491  dvloglem  20492  logf1o2  20494  efopnlem1  20500  logtayl2  20506  cxpcn  20582  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  atandmneg  20699  atandmcj  20702  cosatan  20714  cosatanne0  20715  birthdaylem1  20743  areacl  20754  cxp2lim  20768  jensenlem2  20779  jensen  20780  wilth  20807  sqff1o  20918  dvdsmulf1o  20932  mersenne  20964  bposlem3  21023  lgsqrlem1  21078  lgsqrlem2  21079  lgsqrlem3  21080  lgsqrlem4  21081  lgseisenlem3  21088  lgsquad2lem2  21096  2sqlem6  21106  chebbnd1  21119  chtppilim  21122  chpchtlim  21126  chpo1ub  21127  rplogsumlem1  21131  rplogsumlem2  21132  dchrmusumlema  21140  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0lema  21161  dchrisum0lem2  21165  selberg3lem2  21205  pntrsumo1  21212  selbergsb  21222  pnt2  21260  ostthlem2  21275  ostth2lem2  21281  uhgra0v  21298  usgra0v  21344  usgra1v  21362  eupagra  21641  ablogrpo  21825  smgrpismgm  21873  mndoissmgrp  21880  nmogtmnf  22224  bnnv  22321  hlobn  22343  hcauseq  22640  hlimseqi  22644  hlimveci  22645  shss  22665  sh0  22671  chsh  22680  lnopf  23315  bdopln  23317  nmopgtmnf  23324  hmopf  23330  lnfnf  23340  unopf1o  23372  elunop2  23469  elpjhmop  23641  stcltrlem1  23732  mdslle1i  23773  mdslle2i  23774  rabexgfGS  23940  ssnnssfz  24101  tospos  24139  xrge0tsmsd  24176  ofldsqr  24193  ofldlt1  24196  ofldchr  24197  lmxrge0  24290  qqhrhm  24326  esumpcvgval  24421  measssd  24522  elmbfmvol2  24570  domprobmeas  24621  ballotlemscr  24729  ballotlemfg  24736  ballotlemfrc  24737  ballotlemfrceq  24739  ballotlemrinv0  24743  subfacval3  24828  pcontop  24865  sconpcon  24867  cvmcn  24902  cvmliftlem10  24934  fundmpss  25336  predel  25397  sltres  25532  funpartfun  25696  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  axcontlem10  25816  outsideofcol  25971  itg2addnc  26158  itg2gt0cn  26159  fnebas  26243  filnetlem3  26299  istotbnd3  26370  totbndmet  26371  sstotbnd2  26373  sstotbnd  26374  equivtotbnd  26377  bndmet  26380  totbndbnd  26388  prdstotbnd  26393  crngorngo  26500  prrngorngo  26551  divrngpr  26553  an3  26587  nacsacs  26653  eldiophelnn0  26712  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.27c  26968  jm3.1lem1  26978  jm3.1lem2  26979  jm3.1lem3  26980  lnmlmod  27045  lbslinds  27171  lnrrng  27184  mncply  27210  psgneu  27297  idomrootle  27379  idomodle  27380  hashgcdlem  27384  stoweidlem14  27630  stoweidlem16  27632  stoweidlem24  27640  stoweidlem39  27655  stoweidlem50  27666  stoweidlem51  27667  stoweidlem54  27670  stoweidlem57  27673  wallispilem3  27683  ndmafv  27871  frgrawopreg  28152  2uasbanh  28359  bnj563  28817  bnj658  28825  bnj667  28826  bnj570  28982  bnj938  29014  bnj1001  29035  bnj1006  29036  bnj1049  29049  bnj1121  29060  bnj1173  29077  bnj1177  29081  bnj1245  29089  bnj1311  29099  bnj1321  29102  bnj1388  29108  bnj1398  29109  bnj1415  29113  bnj1417  29116  bnj1421  29117  bnj1442  29124  bnj1452  29127  bnj1489  29131  bnj1312  29133  ollat  29696  omlol  29723  cvlatl  29808  hlomcmcv  29839  2dim  29952  1dimN  29953  lcfl8b  31987  lclkrlem2  32015  lclkrslem1  32020  lclkrslem2  32021  lcfrlem9  32033  mapdval2N  32113  mapdordlem2  32120  mapdrvallem2  32128

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361