Theorem simplbi 476

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  an3  868  3simpa  1058  xoror  1471  sbequ2  1882  rabidim1  3117  reurex  3160  eqimss  3657  pssss  3702  eldifi  3732  elinel1  3799  ssunsn2  4359  pwssun  5020  sopo  5052  wefr  5104  opelxp1  5150  relop  5272  ssrelrn  5315  ordtr  5737  funmo  5904  funrel  5905  fnfun  5988  ffn  6045  f1f  6101  f1of1  6136  f1ofo  6144  isof1o  6573  eqopi  7202  1st2nd2  7205  reldmtpos  7360  swoer  7772  erdisj  7794  ecopover  7851  ecopoverOLD  7852  sdomdom  7983  mapfien  8313  inf3lemd  8524  cardprclem  8805  infxpenlem  8836  cardinfima  8920  dfac5lem4  8949  domtriomlem  9264  smobeth  9408  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  axrnegex  9983  axpre-sup  9990  zre  11381  nnssz  11397  ixxss1  12193  ixxss2  12194  ixxss12  12195  lbioo  12206  ubioo  12207  iccss2  12244  rge0ssre  12280  elfzuz  12338  uzdisj  12413  nn0disj  12455  0wrd0  13331  splfv1  13506  sqrlem6  13988  rlimf  14232  lo1f  14249  lo1dm  14250  o1f  14260  o1dm  14261  mertenslem2  14617  fprodge0  14724  divalglem9  15124  bitsinv2  15165  bitsf1ocnv  15166  gcdcllem1  15221  coprmproddvdslem  15376  prmnn  15388  prmuz2  15408  phimullem  15484  hashgcdlem  15493  1arith  15631  ramtlecl  15704  0ramcl  15727  firest  16093  acsmre  16313  posprs  16949  latpos  17050  clatpos  17110  dlatl  17195  pslem  17206  tsrlemax  17220  tsrps  17221  sgrpmgm  17289  mndsgrp  17299  grpmnd  17429  nsgsubg  17626  ghmgrp1  17662  ghmgrp2  17663  gimghm  17706  gagrp  17725  gaset  17726  psgneu  17926  efgredeu  18165  ablgrp  18198  cmnmnd  18208  cyggenod2  18287  cyggrp  18291  ablfac2  18488  crngring  18558  dvdsrcl  18649  unitcl  18659  brric2  18745  drngring  18754  subrgring  18783  subrgrcl  18785  srngrhm  18851  lmimlmhm  19064  lveclmod  19106  2idlcpbl  19234  qus1  19235  qusrhm  19237  lpirring  19252  nzrring  19261  domnnzr  19295  fldidom  19305  assalmod  19319  assaring  19320  assasca  19321  cygznlem1  19915  cygznlem3  19918  lbslinds  20172  gsummatr01lem1  20461  topontop  20718  tpstop  20741  clsval2  20854  mretopd  20896  neiptoptop  20935  perftop  20960  restfpw  20983  cntop1  21044  cntop2  21045  cnptop1  21046  cnptop2  21047  cnprcl  21049  t1ficld  21131  t0top  21133  t1top  21134  haustop  21135  regtop  21137  nrmtop  21140  cnrmtop  21141  pnrmnrm  21144  cmptop  21198  discmp  21201  tgcmp  21204  uncmp  21206  conndisj  21219  conntop  21220  1stctop  21246  llytop  21275  nllytop  21276  hmeocn  21563  filfbas  21652  ufilfil  21708  flimtop  21769  flimfil  21773  alexsublem  21848  ptcmplem3  21858  tsmsfbas  21931  tsmslem1  21932  tsmsgsum  21942  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  tsmsmhm  21949  tsmsadd  21950  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  tlmtmd  21990  tlmlmod  21992  tlmtrg  21993  tvctlm  22000  ressust  22068  uspreg  22078  ucncn  22089  neipcfilu  22100  cuspusp  22104  isxmet2d  22132  metxmet  22139  xmstps  22258  msxms  22259  xmsxmet  22261  msmet  22262  stdbdxmet  22320  nrgngp  22466  nlmngp  22481  nlmlmod  22482  nlmnrg  22483  nvcnlm  22500  nmoi  22532  nghmrcl1  22536  nghmrcl2  22537  nmhmrcl1  22551  nmhmrcl2  22552  qdensere  22573  xrge0gsumle  22636  xrge0tsms  22637  metds0  22653  metdstri  22654  metdsre  22656  metdseq0  22657  metdscnlem  22658  metnrmlem1a  22661  metnrmlem1  22662  icopnfcnv  22741  cvsclm  22926  cmetmet  23084  cmsms  23145  hlbn  23159  ovolicc2lem5  23289  mblss  23299  mbff  23394  mbfres  23411  mbfadd  23428  mbfsub  23429  i1fmbf  23442  mbfmul  23493  bddmulibl  23605  limcmpt  23647  c1liplem1  23759  c1lip2  23761  fta1glem1  23925  fta1glem2  23926  fta1g  23927  fta1b  23929  ply1pid  23939  aacn  24072  ulmf2  24138  logdmnrp  24387  logdmss  24388  logcnlem2  24389  logcnlem3  24390  logcnlem4  24391  logcnlem5  24392  logcn  24393  dvloglem  24394  logf1o2  24396  efopnlem1  24402  logtayl2  24408  cxpcn  24486  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  atandmneg  24633  atandmcj  24636  cosatan  24648  cosatanne0  24649  birthdaylem1  24678  areacl  24689  cxp2lim  24703  jensenlem2  24714  jensen  24715  sqff1o  24908  dvdsmulf1o  24920  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  lgseisenlem3  25102  chebbnd1  25161  chtppilim  25164  chpchtlim  25168  chpo1ub  25169  dchrmusumlema  25182  dchrvmasumiflem1  25190  dchrisum0lema  25203  dchrisum0lem2  25207  selberg3lem2  25247  pntrsumo1  25254  selbergsb  25264  pnt2  25302  tglineeltr  25526  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  uhgr0vb  25967  lfuhgr1v0e  26146  fusgrusgr  26214  nbupgruvtxres  26308  cusgrusgr  26315  trliswlk  26594  clwlkiswlk  26670  eupthistrl  27071  frgrusgr  27124  ablogrpo  27401  bnnv  27722  hlobn  27744  hcauseq  28042  hlimseqi  28046  hlimveci  28047  shss  28067  sh0  28073  chsh  28081  lnopf  28718  bdopln  28720  hmopf  28733  lnfnf  28743  unopf1o  28775  elunop2  28872  elpjhmop  29044  stcltrlem1  29135  mdslle1i  29176  mdslle2i  29177  rabexgfGS  29340  ssnnssfz  29549  tospos  29658  ogrpgrp  29703  ogrpinvOLD  29715  xrge0tsmsd  29785  ofldfld  29810  ofldlt1  29813  ofldchr  29814  isarchiofld  29817  reofld  29840  rearchi  29842  creftop  29913  lmxrge0  29998  qqhrhm  30033  esumpcvgval  30140  dynkin  30230  measssd  30278  elmbfmvol2  30329  omssubadd  30362  sibfinima  30401  eulerpartlemr  30436  eulerpartlemgf  30441  fiblem  30460  domprobmeas  30472  ballotlemscr  30580  ballotlemfg  30587  ballotlemfrc  30588  ballotlemfrceq  30590  ballotlemrinv0  30594  chtvalz  30707  bnj563  30813  bnj658  30821  bnj667  30822  bnj570  30975  bnj938  31007  bnj1001  31028  bnj1006  31029  bnj1049  31042  bnj1121  31053  bnj1173  31070  bnj1177  31074  bnj1245  31082  bnj1311  31092  bnj1321  31095  bnj1388  31101  bnj1398  31102  bnj1415  31106  bnj1417  31109  bnj1421  31110  bnj1442  31117  bnj1452  31120  bnj1489  31124  bnj1312  31126  pconntop  31207  sconnpconn  31209  cvmcn  31244  cvmliftlem10  31276  fundmpss  31664  sltres  31815  noseponlem  31817  funpartfun  32050  outsideofcol  32240  fnebas  32339  filnetlem3  32375  phpreu  33393  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  poimirlem26  33435  itg2addnc  33464  istotbnd3  33570  totbndmet  33571  sstotbnd2  33573  sstotbnd  33574  equivtotbnd  33577  bndmet  33580  totbndbnd  33588  prdstotbnd  33593  smgrpismgmOLD  33661  mndoissmgrpOLD  33667  crngorngo  33799  prrngorngo  33850  divrngpr  33852  ollat  34500  omlol  34527  cvlatl  34612  hlomcmcv  34643  2dim  34756  1dimN  34757  lcfl8b  36793  lclkrlem2  36821  lclkrslem1  36826  lclkrslem2  36827  lcfrlem9  36839  mapdval2N  36919  mapdordlem2  36926  mapdrvallem2  36934  nacsacs  37272  eldiophelnn0  37327  lnmlmod  37649  lnrring  37682  mncply  37707  idomrootle  37773  idomodle  37774  areaquad  37802  nznngen  38515  binomcxplemcvg  38553  2uasbanh  38777  fompt  39379  disjinfi  39380  climxrre  39982  mbfdmssre  40217  stoweidlem14  40231  stoweidlem16  40233  stoweidlem24  40241  stoweidlem51  40268  stoweidlem54  40271  etransclem32  40483  sge0fodjrnlem  40633  preimagelt  40912  preimalegt  40913  pimrecltpos  40919  pimrecltneg  40933  smfaddlem1  40971  smflimsuplem7  41032  ndmafv  41220  evenz  41543  oddz  41544  gbeeven  41642  gbowodd  41643  rnghmsubcsetclem1  41975  funcrngcsetcALT  41999  rhmsubcsetclem1  42021  rhmsubcrngclem1  42027  ssnn0ssfz  42127  elbigof  42348  digvalnn0  42393