Theorem simplbi 501

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi	⊢ (𝜑 → 𝜓)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 499	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an3  671  xoror  1541  just1-df  2089  dfsbimp  2095  euex  2607  reurex  3374  rabidim1  3439  pssss  4054  eldifi  4087  elinel1  4156  ssunsn2  4788  pwssun  5543  sopo  5578  wefr  5641  opelxp1  5693  relop  5826  ssrelrn  5874  ordtr  6363  funmo  6541  funrel  6542  fnfun  6625  ffn  6695  f1f  6764  f1of1  6809  f1ofo  6818  isof1o  7311  eqopi  8010  1st2nd2  8013  reldmtpos  8218  brinxper  8712  swoer  8714  ecopover  8807  sdomdom  8965  mapfien  9356  inf3lemd  9584  cardprclem  9953  infxpenlem  9985  cardinfima  10069  dfac5lem4  10098  domtriomlem  10414  smobeth  10559  fpwwe2lem5  10608  fpwwe2lem6  10609  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  axrnegex  11135  axpre-sup  11142  zre  12583  ixxss1  13378  ixxss2  13379  ixxss12  13380  lbioo  13391  ubioo  13392  iccss2  13432  rge0ssre  13471  elfzuz  13536  0wrd0  14565  01sqrexlem6  15286  rlimf  15540  lo1f  15557  lo1dm  15558  o1f  15568  o1dm  15569  mertenslem2  15927  divalglem9  16447  bitsinv2  16489  bitsf1ocnv  16490  gcdcllem1  16545  coprmproddvdslem  16708  prmnn  16720  prmuz2  16742  phimullem  16826  hashgcdlem  16835  1arith  16975  ramtlecl  17048  0ramcl  17071  firest  17473  acsmre  17696  posprs  18360  tospos  18462  latpos  18482  clatpos  18545  dlatl  18568  pslem  18616  tsrlemax  18630  tsrps  18631  chnwrd  18652  sgrpmgm  18770  mndsgrp  18786  grpmnd  18995  nsgsubg  19212  ghmgrp1  19276  ghmgrp2  19277  gimghm  19322  gagrp  19350  gaset  19351  psgneu  19564  efgredeu  19810  ablgrp  19843  cmnmnd  19855  cyggenod2  19943  cyggrp  19948  dprd2dlem1  20101  dprd2da  20102  ablfac2  20149  simpggrp  20154  ogrpgrp  20183  crngring  20315  dvdsrcl  20435  unitcl  20445  rimrhm  20564  brric2  20577  nzrringOLD  20588  subrgring  20647  subrgrcl  20649  rnghmsubcsetclem1  20704  funcrngcsetcALT  20714  rhmsubcsetclem1  20733  rhmsubcrngclem1  20739  domnnzr  20779  drngring  20808  flddrngd  20813  rng1nfld  20848  srngrhm  20914  ofldfld  20941  ofldlt1  20944  lmimlmhm  21151  lveclmod  21193  2idlelbas  21362  rng2idlsubgsubrng  21366  2idlcpblrng  21369  2idlcpbl  21370  qus1  21372  qusrhm  21374  lpirring  21456  cygznlem1  21673  cygznlem3  21676  ofldchr  21683  lbslinds  21940  assalmod  21967  assaring  21968  gsummatr01lem1  22769  topontop  23027  tpstop  23051  mretopd  23206  neiptoptop  23245  perftop  23270  restfpw  23293  cntop1  23354  cntop2  23355  cnptop1  23356  cnptop2  23357  cnprcl  23359  t1ficld  23441  t0top  23443  t1top  23444  haustop  23445  regtop  23447  nrmtop  23450  cnrmtop  23451  pnrmnrm  23454  cmptop  23509  tgcmp  23515  conndisj  23530  conntop  23531  1stctop  23557  llytop  23586  nllytop  23587  hmeocn  23874  filfbas  23962  ufilfil  24018  flimtop  24079  flimfil  24083  alexsublem  24158  ptcmplem3  24168  tsmsfbas  24242  tsmslem1  24243  tsmsgsum  24253  tsmssubm  24257  tsmsres  24258  tsmsf1o  24259  tsmsmhm  24260  tsmsadd  24261  tsmsxplem1  24267  tsmsxplem2  24268  tsmsxp  24269  tlmtmd  24301  tlmlmod  24303  tlmtrg  24304  tvctlm  24311  ressust  24377  uspreg  24387  ucncn  24398  neipcfilu  24409  cuspusp  24413  metxmet  24448  xmstps  24567  msxms  24568  xmsxmet  24570  msmet  24571  nrgngp  24776  nlmngp  24791  nlmlmod  24792  nlmnrg  24793  nvcnlm  24810  nmoi  24842  nghmrcl1  24846  nghmrcl2  24847  nmhmrcl1  24861  nmhmrcl2  24862  qdensere  24883  xrge0gsumle  24948  xrge0tsms  24949  icopnfcnv  25058  cvsclm  25242  cphsscph  25367  cmetmet  25402  cmsms  25464  hlbn  25479  ovolicc2lem5  25637  mblss  25647  mbff  25741  mbfres  25760  i1fmbf  25791  limcmpt  25999  c1liplem1  26112  c1lip2  26114  fta1glem1  26282  fta1glem2  26283  fta1g  26284  fta1b  26286  idomrootle  26287  ply1pid  26297  aacn  26435  ulmf2  26501  logdmnrp  26760  logdmss  26761  logcnlem2  26762  logcnlem3  26763  logcnlem4  26764  logcnlem5  26765  logcn  26766  dvloglem  26767  logf1o2  26769  efopnlem1  26775  logtayl2  26781  cxpcn  26864  cxpcn3lem  26866  cxpcn3  26867  resqrtcn  26868  atandmneg  27025  atandmcj  27028  cosatan  27040  cosatanne0  27041  birthdaylem1  27070  areacl  27081  cxp2lim  27095  jensenlem2  27106  jensen  27107  sqff1o  27300  mpodvdsmulf1o  27312  dvdsmulf1o  27314  lgsqrlem1  27464  lgsqrlem2  27465  lgsqrlem3  27466  lgsqrlem4  27467  lgseisenlem3  27495  chebbnd1  27590  chtppilim  27593  chpchtlim  27597  chpo1ub  27598  dchrmusumlema  27611  dchrvmasumiflem1  27619  dchrisum0lema  27632  dchrisum0lem2  27636  selberg3lem2  27676  pntrsumo1  27683  selbergsb  27693  pnt2  27731  ltsres  27780  noseponlem  27782  reno  28639  tglineeltr  28854  axcontlem2  29220  axcontlem7  29225  axcontlem8  29226  uhgr0vb  29327  lfuhgr1v0e  29509  fusgrusgr  29577  uvtxisvtx  29644  nbupgruvtxres  29662  cusgrusgr  29674  trliswlk  29950  clwlkiswlk  30028  clwwlkclwwlkn  30286  eupthistrl  30467  frgrusgr  30517  frgrwopreglem5  30577  clwwnonrepclwwnon  30601  ablogrpo  30804  bnnv  31123  hlobn  31145  hcauseq  31442  hlimseqi  31446  hlimveci  31447  shss  31467  sh0  31473  chsh  31481  lnopf  32116  bdopln  32118  hmopf  32131  lnfnf  32141  unopf1o  32173  elunop2  32270  elpjhmop  32442  stcltrlem1  32533  mdslle1i  32574  mdslle2i  32575  2reu2rex1  32733  2reureurex  32734  ssnnssfz  33040  xrge0tsmsd  33301  isarchiofld  33427  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem4  33473  isdrng4  33526  reofld  33573  rearchi  33576  quslsm  33625  ufdidom  33744  mplvrpmga  33847  srafldlvec  33888  extdggt0  33959  fldextid  33961  extdgid  33962  extdgmul  33965  extdg1id  33968  ist0cld  34135  creftop  34148  lmxrge0  34254  qqhrhm  34291  esumpcvgval  34380  dynkin  34469  measssd  34517  elmbfmvol2  34569  omssubadd  34602  sibfinima  34641  eulerpartlemr  34676  eulerpartlemgf  34681  fiblem  34700  domprobmeas  34712  ballotlemscr  34821  ballotlemfg  34828  ballotlemfrc  34829  ballotlemfrceq  34831  ballotlemrinv0  34835  chtvalz  34928  bnj563  35044  bnj658  35052  bnj667  35053  bnj570  35205  bnj938  35237  bnj1001  35259  bnj1006  35260  bnj1049  35274  bnj1121  35285  bnj1173  35302  bnj1177  35306  bnj1245  35314  bnj1311  35324  bnj1321  35327  bnj1388  35333  bnj1398  35334  bnj1415  35338  bnj1417  35341  bnj1421  35342  bnj1442  35349  bnj1452  35352  bnj1489  35356  bnj1312  35358  pthacycspth  35515  pconntop  35583  sconnpconn  35585  cvmcn  35620  cvmliftlem10  35652  sate0fv0  35775  fundmpss  36125  txpss3v  36234  pprodss4v  36240  outsideofcol  36491  fnebas  36712  filnetlem3  36748  bj-nnfe  37213  bj-xpcossxp  37688  bj-rvecmod  37794  pibt2  37918  phpreu  38110  matunitlindflem1  38122  matunitlindflem2  38123  matunitlindf  38124  poimirlem26  38152  itg2addnc  38180  istotbnd3  38277  totbndmet  38278  sstotbnd2  38280  sstotbnd  38281  equivtotbnd  38284  bndmet  38287  totbndbnd  38295  prdstotbnd  38300  smgrpismgmOLD  38368  mndoissmgrpOLD  38374  crngorngo  38506  prrngorngo  38557  divrngpr  38559  xrnss3v  38887  dfxrn2  38891  refressn  39039  antisymressn  39040  symrelim  39149  eqvrelsym  39195  eqvreltr  39197  disjimeceqim  39310  disjorimxrn  39354  disjim  39390  disjlem14  39407  ollat  39844  omlol  39871  cvlatl  39956  hlomcmcv  39987  2dim  40101  1dimN  40102  lcfl8b  42135  lclkrlem2  42163  lclkrslem1  42168  lclkrslem2  42169  lcfrlem9  42181  mapdval2N  42261  mapdordlem2  42268  mapdrvallem2  42276  idomnnzgmulnz  42757  aks6d1c6lem3  42796  readvrec2  42977  readvrec  42978  readvcot  42980  nacsacs  43297  eldiophelnn0  43352  lnmlmod  43663  lnrring  43696  mncply  43721  idomodle  43775  areaquad  43800  dfno2  44011  harval3  44121  alephiso3  44142  mnurndlem1  44850  nznngen  44885  binomcxplemcvg  44923  2uasbanh  45129  relpf  45518  disjinfi  45769  climxrre  46323  mbfdmssre  46573  stoweidlem14  46587  stoweidlem16  46589  stoweidlem24  46597  stoweidlem51  46624  stoweidlem54  46627  etransclem32  46839  sge0fodjrnlem  46989  pimrecltpos  47281  pimrecltneg  47297  smfaddlem1  47336  smflimsuplem7  47399  ndmafv  47733  dfafv23  47846  dfatcolem  47848  dfatco  47849  evenz  48251  oddz  48252  gbeeven  48375  gbowodd  48376  sclnbgrisvtx  48470  grlimgredgex  48621  ssnn0ssfz  48981  elbigof  49186  digvalnn0  49231  2sphere  49381  mof0  49468  mof0ALT  49470  uobeq2  50031  thincc  50052  termcthin  50107