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  993  xoror  1367  sbequ2  1713  reurex  3078  eqimss  3556  pssss  3599  eldifi  3626  inss1  3718  ssunsn2  4186  pwssun  4786  sopo  4817  wefr  4869  ordtr  4892  opelxp1  5032  relop  5153  xpdifid  5435  funmo  5604  funrel  5605  fnfun  5678  ffn  5731  f1f  5781  f1of1  5815  f1ofo  5823  isof1o  6209  eqopi  6818  1st2nd2  6821  reldmtpos  6963  swoer  7339  erdisj  7359  ecopover  7415  sdomdom  7543  mapfien  7867  inf3lemd  8044  mapfienOLD  8138  cardprclem  8360  infxpenlem  8391  cardinfima  8478  dfac5lem4  8507  domtriomlem  8822  smobeth  8961  fpwwe2lem6  9013  fpwwe2lem7  9014  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  axrnegex  9539  axpre-sup  9546  zre  10868  nnssz  10884  ixxss1  11547  ixxss2  11548  ixxss12  11549  lbioo  11560  ubioo  11561  iccss2  11595  rge0ssre  11628  elfzuz  11684  uzdisj  11751  nn0disj  11788  0wrd0  12532  splfv1  12694  sqrlem6  13044  rlimf  13287  lo1f  13304  lo1dm  13305  o1f  13315  o1dm  13316  fsumge0  13572  mertenslem2  13657  divalglem9  13918  bitsinv2  13952  bitsf1ocnv  13953  gcdcllem1  14008  prmnn  14079  prmind2  14087  nprm  14090  prmuz2  14094  isprm6  14109  exprmfct  14110  isprm5  14112  maxprmfct  14113  phibndlem  14159  phibnd  14160  dfphi2  14163  phimullem  14168  pclem  14221  pcprendvds2  14224  pcpre1  14225  expnprm  14280  prmreclem1  14293  1arith  14304  4sqlem15  14336  4sqlem16  14337  vdwlem5  14362  vdwlem6  14363  vdwlem8  14365  vdwlem9  14366  vdwlem11  14368  ramtlecl  14377  0ramcl  14400  firest  14688  acsmre  14907  posprs  15436  latpos  15537  clatpos  15597  dlatl  15682  pslem  15693  tsrlemax  15707  tsrps  15708  mndlem1  15736  grpmnd  15872  nsgsubg  16038  ghmgrp1  16074  ghmgrp2  16075  gimghm  16117  gagrp  16135  gaset  16136  psgneu  16337  efgredeu  16576  ablgrp  16609  cmnmnd  16619  cyggenod2  16691  cyggrp  16695  ablfac2  16942  crngrng  17010  dvdsrcl  17099  unitcl  17109  brric2  17194  drngrng  17203  subrgrng  17232  subrgrcl  17234  srngrhm  17300  lmimlmhm  17510  lveclmod  17552  2idlcpbl  17681  divs1  17682  divsrhm  17684  lpirrng  17699  nzrrng  17708  domnnzr  17743  fldidom  17753  assalmod  17767  assarng  17768  assasca  17769  cygznlem1  18400  cygznlem3  18403  lbslinds  18663  gsummatr01lem1  18952  topontop  19222  tpstop  19235  clsval2  19345  mretopd  19387  neiptoptop  19426  perftop  19451  restfpw  19474  cntop1  19535  cntop2  19536  cnptop1  19537  cnptop2  19538  cnprcl  19540  t1ficld  19622  t0top  19624  t1top  19625  haustop  19626  regtop  19628  nrmtop  19631  cnrmtop  19632  pnrmnrm  19635  cmptop  19689  discmp  19692  tgcmp  19695  uncmp  19697  conndisj  19711  contop  19712  1stctop  19738  llytop  19767  nllytop  19768  hmeocn  20024  filfbas  20112  ufilfil  20168  flimtop  20229  flimfil  20233  alexsublem  20307  ptcmplem3  20317  tsmsfbas  20389  tsmslem1  20390  tsmsgsum  20400  tsmsgsumOLD  20403  tsmssubm  20407  tsmsresOLD  20408  tsmsres  20409  tsmsf1o  20410  tsmsmhm  20411  tsmsadd  20412  tsmsxplem1  20418  tsmsxplem2  20419  tsmsxp  20420  tlmtmd  20452  tlmlmod  20454  tlmtrg  20455  tvctlm  20462  ressust  20530  uspreg  20540  ucncn  20551  neipcfilu  20562  cuspusp  20566  isxmet2d  20593  metxmet  20600  xmstps  20719  msxms  20720  xmsxmet  20722  msmet  20723  stdbdxmet  20781  nrgngp  20934  nlmngp  20949  nlmlmod  20950  nlmnrg  20951  nvcnlm  20967  nmoi  20998  nghmrcl1  21002  nghmrcl2  21003  nmhmrcl1  21017  nmhmrcl2  21018  qdensere  21040  xrge0gsumle  21101  xrge0tsms  21102  metds0  21117  metdstri  21118  metdsre  21120  metdseq0  21121  metdscnlem  21122  metnrmlem1a  21125  metnrmlem1  21126  icopnfcnv  21205  icopnfhmeo  21206  cvsclm  21370  cmetmet  21488  cmsms  21550  hlbn  21566  ovolicc1  21690  ovolicc2lem5  21695  mblss  21705  mbff  21797  mbfres  21814  mbfadd  21831  mbfsub  21832  i1fmbf  21845  mbfmul  21896  bddmulibl  22008  limcmpt  22050  c1liplem1  22160  c1lip2  22162  fta1glem1  22329  fta1glem2  22330  fta1g  22331  fta1b  22333  ply1pid  22343  aacn  22475  ulmf2  22541  logdmnrp  22778  logdmss  22779  logcnlem2  22780  logcnlem3  22781  logcnlem4  22782  logcnlem5  22783  logcn  22784  dvloglem  22785  logf1o2  22787  efopnlem1  22793  logtayl2  22799  cxpcn  22875  cxpcn3lem  22877  cxpcn3  22878  resqrtcn  22879  atandmneg  22993  atandmcj  22996  cosatan  23008  cosatanne0  23009  birthdaylem1  23037  areacl  23048  cxp2lim  23062  jensenlem2  23073  jensen  23074  wilth  23101  sqff1o  23212  dvdsmulf1o  23226  mersenne  23258  bposlem3  23317  lgsqrlem1  23372  lgsqrlem2  23373  lgsqrlem3  23374  lgsqrlem4  23375  lgseisenlem3  23382  lgsquad2lem2  23390  2sqlem6  23400  chebbnd1  23413  chtppilim  23416  chpchtlim  23420  chpo1ub  23421  rplogsumlem1  23425  rplogsumlem2  23426  dchrmusumlema  23434  dchrvmasumiflem1  23442  dchrisum0flblem2  23450  dchrisum0lema  23455  dchrisum0lem2  23459  selberg3lem2  23499  pntrsumo1  23506  selbergsb  23516  pnt2  23554  ostthlem2  23569  ostth2lem2  23575  tglineeltr  23753  axcontlem2  23972  axcontlem7  23977  axcontlem8  23978  axcontlem10  23980  uhgra0v  24014  usgra0v  24075  usgra1v  24094  rusgranumwlks  24660  eupagra  24670  frgrawopreg  24754  ablogrpo  24990  smgrpismgm  25038  mndoissmgrp  25045  nmogtmnf  25389  bnnv  25486  hlobn  25508  hcauseq  25806  hlimseqi  25810  hlimveci  25811  shss  25831  sh0  25837  chsh  25846  lnopf  26482  bdopln  26484  nmopgtmnf  26491  hmopf  26497  lnfnf  26507  unopf1o  26539  elunop2  26636  elpjhmop  26808  stcltrlem1  26899  mdslle1i  26940  mdslle2i  26941  rabexgfGS  27105  suppss3  27250  ssnnssfz  27293  tospos  27336  ogrpgrp  27383  ogrpinvOLD  27395  ogrpinv0le  27396  ogrpsub  27397  ogrpaddlt  27398  archirng  27422  archirngz  27423  archiabllem1a  27425  archiabllem1b  27426  archiabllem1  27427  archiabllem2a  27428  archiabllem2c  27429  archiabllem2b  27430  archiabllem2  27431  xrge0tsmsd  27466  ofldfld  27491  ofldlt1  27494  ofldchr  27495  isarchiofld  27498  reofld  27521  rearchi  27523  lmxrge0  27598  qqhrhm  27634  esumpcvgval  27752  measssd  27854  elmbfmvol2  27906  sibfinima  27949  eulerpartlemr  27981  eulerpartlemgf  27986  fiblem  28005  domprobmeas  28017  ballotlemscr  28125  ballotlemfg  28132  ballotlemfrc  28133  ballotlemfrceq  28135  ballotlemrinv0  28139  signstfveq0  28202  subfacval3  28301  pcontop  28338  sconpcon  28340  cvmcn  28375  cvmliftlem10  28407  fundmpss  28801  predel  28868  sltres  29029  funpartfun  29198  outsideofcol  29388  itg2addnc  29674  itg2gt0cn  29675  ftc1anclem3  29697  fnebas  29773  filnetlem3  29829  istotbnd3  29898  totbndmet  29899  sstotbnd2  29901  sstotbnd  29902  equivtotbnd  29905  bndmet  29908  totbndbnd  29916  prdstotbnd  29921  crngorngo  30028  prrngorngo  30079  divrngpr  30081  an3  30223  nacsacs  30273  eldiophelnn0  30329  jm2.17a  30530  jm2.17b  30531  jm2.17c  30532  jm2.27c  30581  jm3.1lem1  30591  jm3.1lem2  30592  jm3.1lem3  30593  lnmlmod  30657  lnrrng  30693  mncply  30719  idomrootle  30785  idomodle  30786  hashgcdlem  30790  areaquad  30817  nznngen  30849  icoiccdif  31156  lptre2pt  31210  icccncfext  31254  dvrecg  31268  stoweidlem14  31342  stoweidlem16  31344  stoweidlem24  31352  stoweidlem39  31367  stoweidlem50  31378  stoweidlem51  31379  stoweidlem54  31382  stoweidlem57  31385  wallispilem3  31395  fourierdlem32  31467  fourierdlem33  31468  fourierdlem48  31483  fourierdlem49  31484  fourierdlem51  31486  fourierdlem62  31497  fourierdlem70  31505  fourierdlem79  31514  ndmafv  31720  uhg0v  31872  sgrpmgm  31956  ssnn0ssfz  32034  2uasbanh  32432  bnj563  32897  bnj658  32905  bnj667  32906  bnj570  33060  bnj938  33092  bnj1001  33113  bnj1006  33114  bnj1049  33127  bnj1121  33138  bnj1173  33155  bnj1177  33159  bnj1245  33167  bnj1311  33177  bnj1321  33180  bnj1388  33186  bnj1398  33187  bnj1415  33191  bnj1417  33194  bnj1421  33195  bnj1442  33202  bnj1452  33205  bnj1489  33209  bnj1312  33211  ollat  34028  omlol  34055  cvlatl  34140  hlomcmcv  34171  2dim  34284  1dimN  34285  lcfl8b  36319  lclkrlem2  36347  lclkrslem1  36352  lclkrslem2  36353  lcfrlem9  36365  mapdval2N  36445  mapdordlem2  36452  mapdrvallem2  36460