Theorem simplbi 467

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  3simpa  1027  xoror  1438  sbequ2  1807  reurex  2995  eqimss  3470  pssss  3514  eldifi  3544  elinel1  3610  elin1d  3613  inss1  3643  ssunsn2  4123  pwssun  4745  sopo  4777  wefr  4829  opelxp1  4872  relop  4990  predel  5404  ordtr  5444  funmo  5605  funrel  5606  fnfun  5683  ffn  5739  f1f  5792  f1of1  5827  f1ofo  5835  isof1o  6234  eqopi  6846  1st2nd2  6849  reldmtpos  6999  swoer  7409  erdisj  7429  ecopover  7485  sdomdom  7615  mapfien  7939  inf3lemd  8150  cardprclem  8431  infxpenlem  8462  cardinfima  8546  dfac5lem4  8575  domtriomlem  8890  smobeth  9029  fpwwe2lem6  9078  fpwwe2lem7  9079  fpwwe2lem12  9084  fpwwe2lem13  9085  fpwwe2  9086  axrnegex  9604  axpre-sup  9611  zre  10965  nnssz  10981  ixxss1  11678  ixxss2  11679  ixxss12  11680  lbioo  11692  ubioo  11693  iccss2  11730  rge0ssre  11766  elfzuz  11822  uzdisj  11893  nn0disj  11932  0wrd0  12744  splfv1  12916  sqrlem6  13388  rlimf  13642  lo1f  13659  lo1dm  13660  o1f  13670  o1dm  13671  mertenslem2  14018  fprodge0  14124  divalglem9  14460  divalglem9OLD  14461  bitsinv2  14496  bitsf1ocnv  14497  gcdcllem1  14552  prmnn  14704  prmuz2  14721  coprmproddvdslem  14758  phimullem  14806  1arith  14950  ramtlecl  15030  0ramcl  15060  firest  15409  acsmre  15636  posprs  16272  latpos  16374  clatpos  16434  dlatl  16519  pslem  16530  tsrlemax  16544  tsrps  16545  sgrpmgm  16610  mndsgrp  16621  grpmnd  16756  nsgsubg  16927  ghmgrp1  16963  ghmgrp2  16964  gimghm  17006  gagrp  17024  gaset  17025  psgneu  17225  efgredeu  17480  ablgrp  17513  cmnmnd  17523  cyggenod2  17598  cyggrp  17602  ablfac2  17800  crngring  17869  dvdsrcl  17955  unitcl  17965  brric2  18051  drngring  18060  subrgring  18089  subrgrcl  18091  srngrhm  18157  lmimlmhm  18365  lveclmod  18407  2idlcpbl  18535  qus1  18536  qusrhm  18538  lpirring  18553  nzrring  18562  domnnzr  18596  fldidom  18606  assalmod  18620  assaring  18621  assasca  18622  cygznlem1  19214  cygznlem3  19217  lbslinds  19468  gsummatr01lem1  19757  topontop  20018  tpstop  20031  clsval2  20142  mretopd  20185  neiptoptop  20224  perftop  20249  restfpw  20272  cntop1  20333  cntop2  20334  cnptop1  20335  cnptop2  20336  cnprcl  20338  t1ficld  20420  t0top  20422  t1top  20423  haustop  20424  regtop  20426  nrmtop  20429  cnrmtop  20430  pnrmnrm  20433  cmptop  20487  discmp  20490  tgcmp  20493  uncmp  20495  conndisj  20508  contop  20509  1stctop  20535  llytop  20564  nllytop  20565  hmeocn  20852  filfbas  20941  ufilfil  20997  flimtop  21058  flimfil  21062  alexsublem  21137  ptcmplem3  21147  tsmsfbas  21220  tsmslem1  21221  tsmsgsum  21231  tsmssubm  21235  tsmsres  21236  tsmsf1o  21237  tsmsmhm  21238  tsmsadd  21239  tsmsxplem1  21245  tsmsxplem2  21246  tsmsxp  21247  tlmtmd  21279  tlmlmod  21281  tlmtrg  21282  tvctlm  21289  ressust  21357  uspreg  21367  ucncn  21378  neipcfilu  21389  cuspusp  21393  isxmet2d  21420  metxmet  21427  xmstps  21546  msxms  21547  xmsxmet  21549  msmet  21550  stdbdxmet  21608  nrgngp  21743  nlmngp  21758  nlmlmod  21759  nlmnrg  21760  nvcnlm  21776  nmoi  21811  nmoiOLD  21827  nghmrcl1  21831  nghmrcl2  21832  nmhmrcl1  21846  nmhmrcl2  21847  qdensere  21868  xrge0gsumle  21929  xrge0tsms  21930  metds0  21945  metdstri  21946  metdsre  21948  metdseq0  21949  metdscnlem  21950  metnrmlem1a  21953  metnrmlem1  21954  metds0OLD  21960  metdstriOLD  21961  metdsreOLD  21963  metdseq0OLD  21964  metdscnlemOLD  21965  metnrmlem1aOLD  21968  metnrmlem1OLD  21969  icopnfcnv  22048  cvsclm  22216  cmetmet  22334  cmsms  22394  hlbn  22408  ovolicc2lem5  22553  mblss  22563  mbff  22662  mbfres  22679  mbfadd  22696  mbfsub  22697  i1fmbf  22712  mbfmul  22763  bddmulibl  22875  limcmpt  22917  c1liplem1  23027  c1lip2  23029  fta1glem1  23195  fta1glem2  23196  fta1g  23197  fta1b  23199  ply1pid  23216  aacn  23349  ulmf2  23418  logdmnrp  23665  logdmss  23666  logcnlem2  23667  logcnlem3  23668  logcnlem4  23669  logcnlem5  23670  logcn  23671  dvloglem  23672  logf1o2  23674  efopnlem1  23680  logtayl2  23686  cxpcn  23764  cxpcn3lem  23766  cxpcn3  23767  resqrtcn  23768  atandmneg  23911  atandmcj  23914  cosatan  23926  cosatanne0  23927  birthdaylem1  23956  areacl  23967  cxp2lim  23981  jensenlem2  23992  jensen  23993  sqff1o  24188  dvdsmulf1o  24202  lgsqrlem1  24348  lgsqrlem2  24349  lgsqrlem3  24350  lgsqrlem4  24351  lgseisenlem3  24358  chebbnd1  24389  chtppilim  24392  chpchtlim  24396  chpo1ub  24397  dchrmusumlema  24410  dchrvmasumiflem1  24418  dchrisum0lema  24431  dchrisum0lem2  24435  selberg3lem2  24475  pntrsumo1  24482  selbergsb  24492  pnt2  24530  tglineeltr  24755  axcontlem2  25074  axcontlem7  25079  axcontlem8  25080  uhgra0v  25116  usgra0v  25177  usgra1v  25196  eupagra  25773  frgrawopreg  25856  ablogrpo  26093  smgrpismgmOLD  26141  mndoissmgrpOLD  26148  bnnv  26589  hlobn  26621  hcauseq  26919  hlimseqi  26923  hlimveci  26924  shss  26944  sh0  26950  chsh  26958  lnopf  27593  bdopln  27595  hmopf  27608  lnfnf  27618  unopf1o  27650  elunop2  27747  elpjhmop  27919  stcltrlem1  28010  mdslle1i  28051  mdslle2i  28052  rabexgfGS  28216  ssnnssfz  28442  tospos  28494  ogrpgrp  28540  ogrpinvOLD  28552  xrge0tsmsd  28622  ofldfld  28647  ofldlt1  28650  ofldchr  28651  isarchiofld  28654  reofld  28677  rearchi  28679  creftop  28747  lmxrge0  28832  qqhrhm  28867  esumpcvgval  28973  dynkin  29063  measssd  29111  elmbfmvol2  29162  omssubadd  29201  omssubaddOLD  29205  sibfinima  29245  eulerpartlemr  29280  eulerpartlemgf  29285  fiblem  29304  domprobmeas  29316  ballotlemscr  29424  ballotlemfg  29431  ballotlemfrc  29432  ballotlemfrceq  29434  ballotlemrinv0  29438  ballotlemscrOLD  29462  ballotlemfgOLD  29469  ballotlemfrcOLD  29470  ballotlemfrceqOLD  29472  ballotlemrinv0OLD  29476  bnj563  29625  bnj658  29633  bnj667  29634  bnj570  29788  bnj938  29820  bnj1001  29841  bnj1006  29842  bnj1049  29855  bnj1121  29866  bnj1173  29883  bnj1177  29887  bnj1245  29895  bnj1311  29905  bnj1321  29908  bnj1388  29914  bnj1398  29915  bnj1415  29919  bnj1417  29922  bnj1421  29923  bnj1442  29930  bnj1452  29933  bnj1489  29937  bnj1312  29939  pcontop  30020  sconpcon  30022  cvmcn  30057  cvmliftlem10  30089  fundmpss  30478  sltres  30622  noseponlem  30626  funpartfun  30781  outsideofcol  30971  fnebas  31071  filnetlem3  31107  phpreu  31993  poimirlem26  32030  itg2addnc  32060  istotbnd3  32167  totbndmet  32168  sstotbnd2  32170  sstotbnd  32171  equivtotbnd  32174  bndmet  32177  totbndbnd  32185  prdstotbnd  32190  crngorngo  32297  prrngorngo  32348  divrngpr  32350  an3  32488  ollat  32850  omlol  32877  cvlatl  32962  hlomcmcv  32993  2dim  33106  1dimN  33107  lcfl8b  35143  lclkrlem2  35171  lclkrslem1  35176  lclkrslem2  35177  lcfrlem9  35189  mapdval2N  35269  mapdordlem2  35276  mapdrvallem2  35284  nacsacs  35622  eldiophelnn0  35677  lnmlmod  36008  lnrring  36042  mncply  36067  idomrootle  36140  idomodle  36141  hashgcdlem  36145  areaquad  36172  nznngen  36735  binomcxplemcvg  36773  2uasbanh  36998  fompt  37538  disjinfi  37539  stoweidlem14  37986  stoweidlem16  37988  stoweidlem24  37996  stoweidlem51  38024  stoweidlem54  38027  etransclem32  38243  sge0fodjrnlem  38372  ndmafv  38787  evenz  38904  oddz  38905  gbeeven  39000  gboodd  39001  ssrelrn  39156  uhgr0vb  39319  usgr1vr  39493  nbupgruvtxres  39644  cusgrusgr  39651  uhg0v  40197  rnghmsubcsetclem1  40485  funcrngcsetcALT  40509  rhmsubcsetclem1  40531  rhmsubcrngclem1  40537  ssnn0ssfz  40638  elbigof  40873  digvalnn0  40918