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  1357  sbequ2  1702  reurex  2932  eqimss  3403  pssss  3446  eldifi  3473  inss1  3565  ssunsn2  4027  pwssun  4622  sopo  4653  wefr  4705  ordtr  4728  opelxp1  4867  relop  4985  xpdifid  5261  funmo  5429  funrel  5430  fnfun  5503  ffn  5554  f1f  5601  f1of1  5635  f1ofo  5643  isof1o  6011  eqopi  6605  1st2nd2  6608  reldmtpos  6748  swoer  7121  erdisj  7140  ecopover  7196  sdomdom  7329  mapfien  7649  inf3lemd  7825  mapfienOLD  7919  cardprclem  8141  infxpenlem  8172  cardinfima  8259  dfac5lem4  8288  domtriomlem  8603  smobeth  8742  fpwwe2lem6  8794  fpwwe2lem7  8795  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  axrnegex  9321  axpre-sup  9328  zre  10642  nnssz  10658  ixxss1  11310  ixxss2  11311  ixxss12  11312  lbioo  11323  ubioo  11324  iccss2  11358  rge0ssre  11385  elfzuz  11441  uzdisj  11523  0wrd0  12245  splfv1  12389  sqrlem6  12729  rlimf  12971  lo1f  12988  lo1dm  12989  o1f  12999  o1dm  13000  fsumge0  13250  mertenslem2  13337  divalglem9  13597  bitsinv2  13631  bitsf1ocnv  13632  gcdcllem1  13687  prmnn  13758  prmind2  13766  nprm  13769  prmuz2  13773  isprm6  13787  exprmfct  13788  isprm5  13790  maxprmfct  13791  phibndlem  13837  phibnd  13838  dfphi2  13841  phimullem  13846  pclem  13897  pcprendvds2  13900  pcpre1  13901  expnprm  13956  prmreclem1  13969  1arith  13980  4sqlem15  14012  4sqlem16  14013  vdwlem5  14038  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  vdwlem11  14044  ramtlecl  14053  0ramcl  14076  firest  14363  acsmre  14582  posprs  15111  latpos  15212  clatpos  15272  dlatl  15357  pslem  15368  tsrlemax  15382  tsrps  15383  mndlem1  15411  grpmnd  15541  nsgsubg  15704  ghmgrp1  15740  ghmgrp2  15741  gimghm  15783  gagrp  15801  gaset  15802  psgneu  16003  efgredeu  16240  ablgrp  16273  cmnmnd  16283  cyggenod2  16353  cyggrp  16357  ablfac2  16580  crngrng  16645  dvdsrcl  16731  unitcl  16741  drngrng  16819  subrgrng  16848  subrgrcl  16850  srngrhm  16916  lmimlmhm  17125  lveclmod  17167  2idlcpbl  17296  divs1  17297  divsrhm  17299  lpirrng  17314  nzrrng  17323  domnnzr  17347  fldidom  17357  assalmod  17371  assarng  17372  assasca  17373  cygznlem1  17979  cygznlem3  17982  lbslinds  18242  gsummatr01lem1  18441  topontop  18511  tpstop  18524  clsval2  18634  mretopd  18676  neiptoptop  18715  perftop  18740  restfpw  18763  cntop1  18824  cntop2  18825  cnptop1  18826  cnptop2  18827  cnprcl  18829  t1ficld  18911  t0top  18913  t1top  18914  haustop  18915  regtop  18917  nrmtop  18920  cnrmtop  18921  pnrmnrm  18924  cmptop  18978  discmp  18981  tgcmp  18984  uncmp  18986  conndisj  19000  contop  19001  1stctop  19027  llytop  19056  nllytop  19057  hmeocn  19313  filfbas  19401  ufilfil  19457  flimtop  19518  flimfil  19522  alexsublem  19596  ptcmplem3  19606  tsmsfbas  19678  tsmslem1  19679  tsmsgsum  19689  tsmsgsumOLD  19692  tsmssubm  19696  tsmsresOLD  19697  tsmsres  19698  tsmsf1o  19699  tsmsmhm  19700  tsmsadd  19701  tsmsxplem1  19707  tsmsxplem2  19708  tsmsxp  19709  tlmtmd  19741  tlmlmod  19743  tlmtrg  19744  tvctlm  19751  ressust  19819  uspreg  19829  ucncn  19840  neipcfilu  19851  cuspusp  19855  isxmet2d  19882  metxmet  19889  xmstps  20008  msxms  20009  xmsxmet  20011  msmet  20012  stdbdxmet  20070  nrgngp  20223  nlmngp  20238  nlmlmod  20239  nlmnrg  20240  nvcnlm  20256  nmoi  20287  nghmrcl1  20291  nghmrcl2  20292  nmhmrcl1  20306  nmhmrcl2  20307  qdensere  20329  xrge0gsumle  20390  xrge0tsms  20391  metds0  20406  metdstri  20407  metdsre  20409  metdseq0  20410  metdscnlem  20411  metnrmlem1a  20414  metnrmlem1  20415  icopnfcnv  20494  icopnfhmeo  20495  cvsclm  20659  cmetmet  20777  cmsms  20839  hlbn  20855  ovolicc1  20979  ovolicc2lem5  20984  mblss  20994  mbff  21085  mbfres  21102  mbfadd  21119  mbfsub  21120  i1fmbf  21133  mbfmul  21184  bddmulibl  21296  limcmpt  21338  c1liplem1  21448  c1lip2  21450  fta1glem1  21617  fta1glem2  21618  fta1g  21619  fta1b  21621  ply1pid  21631  aacn  21763  ulmf2  21829  logdmnrp  22066  logdmss  22067  logcnlem2  22068  logcnlem3  22069  logcnlem4  22070  logcnlem5  22071  logcn  22072  dvloglem  22073  logf1o2  22075  efopnlem1  22081  logtayl2  22087  cxpcn  22163  cxpcn3lem  22165  cxpcn3  22166  resqrcn  22167  atandmneg  22281  atandmcj  22284  cosatan  22296  cosatanne0  22297  birthdaylem1  22325  areacl  22336  cxp2lim  22350  jensenlem2  22361  jensen  22362  wilth  22389  sqff1o  22500  dvdsmulf1o  22514  mersenne  22546  bposlem3  22605  lgsqrlem1  22660  lgsqrlem2  22661  lgsqrlem3  22662  lgsqrlem4  22663  lgseisenlem3  22670  lgsquad2lem2  22678  2sqlem6  22688  chebbnd1  22701  chtppilim  22704  chpchtlim  22708  chpo1ub  22709  rplogsumlem1  22713  rplogsumlem2  22714  dchrmusumlema  22722  dchrvmasumiflem1  22730  dchrisum0flblem2  22738  dchrisum0lema  22743  dchrisum0lem2  22747  selberg3lem2  22787  pntrsumo1  22794  selbergsb  22804  pnt2  22842  ostthlem2  22857  ostth2lem2  22863  tglineeltr  23017  axcontlem2  23179  axcontlem7  23184  axcontlem8  23185  axcontlem10  23187  uhgra0v  23212  usgra0v  23258  usgra1v  23276  eupagra  23555  ablogrpo  23739  smgrpismgm  23787  mndoissmgrp  23794  nmogtmnf  24138  bnnv  24235  hlobn  24257  hcauseq  24555  hlimseqi  24559  hlimveci  24560  shss  24580  sh0  24586  chsh  24595  lnopf  25231  bdopln  25233  nmopgtmnf  25240  hmopf  25246  lnfnf  25256  unopf1o  25288  elunop2  25385  elpjhmop  25557  stcltrlem1  25648  mdslle1i  25689  mdslle2i  25690  rabexgfGS  25854  suppss3  25995  ssnnssfz  26044  tospos  26087  ogrpgrp  26134  ogrpinvOLD  26146  ogrpinv0le  26147  ogrpsub  26148  ogrpaddlt  26149  archirng  26173  archirngz  26174  archiabllem1a  26176  archiabllem1b  26177  archiabllem1  26178  archiabllem2a  26179  archiabllem2c  26180  archiabllem2b  26181  archiabllem2  26182  xrge0tsmsd  26221  ofldfld  26246  ofldlt1  26249  ofldchr  26250  isarchiofld  26253  reofld  26277  rearchi  26279  lmxrge0  26351  qqhrhm  26387  esumpcvgval  26496  measssd  26598  elmbfmvol2  26651  sibfinima  26694  eulerpartlemr  26726  eulerpartlemgf  26731  fiblem  26750  domprobmeas  26762  ballotlemscr  26870  ballotlemfg  26877  ballotlemfrc  26878  ballotlemfrceq  26880  ballotlemrinv0  26884  signstfveq0  26947  subfacval3  27046  pcontop  27083  sconpcon  27085  cvmcn  27120  cvmliftlem10  27152  fundmpss  27546  predel  27613  sltres  27774  funpartfun  27943  outsideofcol  28133  itg2addnc  28417  itg2gt0cn  28418  ftc1anclem3  28440  fnebas  28516  filnetlem3  28572  istotbnd3  28641  totbndmet  28642  sstotbnd2  28644  sstotbnd  28645  equivtotbnd  28648  bndmet  28651  totbndbnd  28659  prdstotbnd  28664  crngorngo  28771  prrngorngo  28822  divrngpr  28824  an3  28966  nacsacs  29016  eldiophelnn0  29073  jm2.17a  29274  jm2.17b  29275  jm2.17c  29276  jm2.27c  29327  jm3.1lem1  29337  jm3.1lem2  29338  jm3.1lem3  29339  lnmlmod  29403  lnrrng  29439  mncply  29465  idomrootle  29531  idomodle  29532  hashgcdlem  29536  areaquad  29563  stoweidlem14  29780  stoweidlem16  29782  stoweidlem24  29790  stoweidlem39  29805  stoweidlem50  29816  stoweidlem51  29817  stoweidlem54  29820  stoweidlem57  29823  wallispilem3  29833  ndmafv  30017  rusgranumwlks  30545  frgrawopreg  30613  ssnn0ssfz  30711  2uasbanh  31199  bnj563  31664  bnj658  31672  bnj667  31673  bnj570  31827  bnj938  31859  bnj1001  31880  bnj1006  31881  bnj1049  31894  bnj1121  31905  bnj1173  31922  bnj1177  31926  bnj1245  31934  bnj1311  31944  bnj1321  31947  bnj1388  31953  bnj1398  31954  bnj1415  31958  bnj1417  31961  bnj1421  31962  bnj1442  31969  bnj1452  31972  bnj1489  31976  bnj1312  31978  ollat  32751  omlol  32778  cvlatl  32863  hlomcmcv  32894  2dim  33007  1dimN  33008  lcfl8b  35042  lclkrlem2  35070  lclkrslem1  35075  lclkrslem2  35076  lcfrlem9  35088  mapdval2N  35168  mapdordlem2  35175  mapdrvallem2  35183