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  1548  euex  2605  reurex  3373  rabidim1  3438  pssss  4053  eldifi  4086  elinel1  4155  ssunsn2  4794  pwssun  5555  sopo  5590  wefr  5653  opelxp1  5705  relop  5838  ssrelrn  5886  ordtr  6376  funmo  6554  funrel  6555  fnfun  6637  ffn  6707  f1f  6776  f1of1  6821  f1ofo  6830  isof1o  7323  eqopi  8023  1st2nd2  8026  reldmtpos  8231  brinxper  8725  swoer  8727  ecopover  8820  sdomdom  8978  mapfien  9369  inf3lemd  9597  cardprclem  9966  infxpenlem  9998  cardinfima  10082  dfac5lem4  10111  domtriomlem  10427  smobeth  10572  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  axrnegex  11148  axpre-sup  11155  zre  12596  ixxss1  13391  ixxss2  13392  ixxss12  13393  lbioo  13404  ubioo  13405  iccss2  13445  rge0ssre  13484  elfzuz  13549  0wrd0  14579  01sqrexlem6  15300  rlimf  15554  lo1f  15571  lo1dm  15572  o1f  15582  o1dm  15583  mertenslem2  15941  divalglem9  16460  bitsinv2  16502  bitsf1ocnv  16503  gcdcllem1  16558  coprmproddvdslem  16721  prmnn  16733  prmuz2  16755  phimullem  16839  hashgcdlem  16848  1arith  16988  ramtlecl  17061  0ramcl  17084  firest  17486  acsmre  17709  posprs  18373  tospos  18475  latpos  18495  clatpos  18558  dlatl  18581  pslem  18629  tsrlemax  18643  tsrps  18644  chnwrd  18665  sgrpmgm  18783  mndsgrp  18799  grpmnd  19008  nsgsubg  19225  ghmgrp1  19289  ghmgrp2  19290  gimghm  19335  gagrp  19363  gaset  19364  psgneu  19577  efgredeu  19823  ablgrp  19856  cmnmnd  19868  cyggenod2  19956  cyggrp  19961  dprd2dlem1  20114  dprd2da  20115  ablfac2  20162  simpggrp  20167  ogrpgrp  20196  crngring  20328  dvdsrcl  20448  unitcl  20458  rimrhm  20577  brric2  20590  nzrringOLD  20601  subrgring  20660  subrgrcl  20662  rnghmsubcsetclem1  20717  funcrngcsetcALT  20727  rhmsubcsetclem1  20746  rhmsubcrngclem1  20752  domnnzr  20792  drngring  20821  isdrng4  20826  flddrngd  20828  rng1nfld  20863  srngrhm  20929  ofldfld  20956  ofldlt1  20959  lmimlmhm  21166  lveclmod  21208  2idlelbas  21384  rng2idlsubgsubrng  21388  2idlcpblrng  21391  2idlcpbl  21392  qus1  21394  qusrhm  21396  lpirring  21480  cygznlem1  21697  cygznlem3  21700  ofldchr  21707  lbslinds  21964  assalmod  21991  assaring  21992  gsummatr01lem1  22793  topontop  23051  tpstop  23075  mretopd  23230  neiptoptop  23269  perftop  23294  restfpw  23317  cntop1  23378  cntop2  23379  cnptop1  23380  cnptop2  23381  cnprcl  23383  t1ficld  23465  t0top  23467  t1top  23468  haustop  23469  regtop  23471  nrmtop  23474  cnrmtop  23475  pnrmnrm  23478  cmptop  23533  tgcmp  23539  conndisj  23554  conntop  23555  1stctop  23581  llytop  23610  nllytop  23611  hmeocn  23898  filfbas  23986  ufilfil  24042  flimtop  24103  flimfil  24107  alexsublem  24182  ptcmplem3  24192  tsmsfbas  24266  tsmslem1  24267  tsmsgsum  24277  tsmssubm  24281  tsmsres  24282  tsmsf1o  24283  tsmsmhm  24284  tsmsadd  24285  tsmsxplem1  24291  tsmsxplem2  24292  tsmsxp  24293  tlmtmd  24325  tlmlmod  24327  tlmtrg  24328  tvctlm  24335  ressust  24401  uspreg  24411  ucncn  24422  neipcfilu  24433  cuspusp  24437  metxmet  24472  xmstps  24591  msxms  24592  xmsxmet  24594  msmet  24595  nrgngp  24800  nlmngp  24815  nlmlmod  24816  nlmnrg  24817  nvcnlm  24834  nmoi  24866  nghmrcl1  24870  nghmrcl2  24871  nmhmrcl1  24885  nmhmrcl2  24886  qdensere  24907  xrge0gsumle  24972  xrge0tsms  24973  icopnfcnv  25082  cvsclm  25266  cphsscph  25391  cmetmet  25426  cmsms  25488  hlbn  25503  ovolicc2lem5  25661  mblss  25671  mbff  25765  mbfres  25784  i1fmbf  25815  limcmpt  26023  c1liplem1  26136  c1lip2  26138  fta1glem1  26306  fta1glem2  26307  fta1g  26308  fta1b  26310  idomrootle  26311  ply1pid  26321  aacn  26459  ulmf2  26528  logdmnrp  26787  logdmss  26788  logcnlem2  26789  logcnlem3  26790  logcnlem4  26791  logcnlem5  26792  logcn  26793  dvloglem  26794  logf1o2  26796  efopnlem1  26802  logtayl2  26808  cxpcn  26891  cxpcn3lem  26893  cxpcn3  26894  resqrtcn  26895  atandmneg  27052  atandmcj  27055  cosatan  27067  cosatanne0  27068  birthdaylem1  27097  areacl  27108  cxp2lim  27122  jensenlem2  27133  jensen  27134  sqff1o  27327  mpodvdsmulf1o  27339  dvdsmulf1o  27341  lgsqrlem1  27491  lgsqrlem2  27492  lgsqrlem3  27493  lgsqrlem4  27494  lgseisenlem3  27522  chebbnd1  27617  chtppilim  27620  chpchtlim  27624  chpo1ub  27625  dchrmusumlema  27638  dchrvmasumiflem1  27646  dchrisum0lema  27659  dchrisum0lem2  27663  selberg3lem2  27703  pntrsumo1  27710  selbergsb  27720  pnt2  27758  ltsres  27807  noseponlem  27809  reno  28666  tglineeltr  28885  axcontlem2  29296  axcontlem7  29301  axcontlem8  29302  uhgr0vb  29403  lfuhgr1v0e  29585  fusgrusgr  29653  uvtxisvtx  29720  nbupgruvtxres  29738  cusgrusgr  29750  trliswlk  30026  clwlkiswlk  30104  clwwlkclwwlkn  30362  eupthistrl  30543  frgrusgr  30593  frgrwopreglem5  30653  clwwnonrepclwwnon  30677  ablogrpo  30880  bnnv  31199  hlobn  31221  hcauseq  31518  hlimseqi  31522  hlimveci  31523  shss  31543  sh0  31549  chsh  31557  lnopf  32192  bdopln  32194  hmopf  32207  lnfnf  32217  unopf1o  32249  elunop2  32346  elpjhmop  32518  stcltrlem1  32609  mdslle1i  32650  mdslle2i  32651  2reu2rex1  32808  2reureurex  32809  ssnnssfz  33113  xrge0tsmsd  33374  isarchiofld  33500  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem4  33546  reofld  33644  rearchi  33647  quslsm  33695  ufdidom  33813  mplvrpmga  33916  srafldlvec  33957  extdggt0  34028  fldextid  34030  extdgid  34031  extdgmul  34034  extdg1id  34037  ist0cld  34204  creftop  34217  lmxrge0  34323  qqhrhm  34360  esumpcvgval  34449  dynkin  34538  measssd  34586  elmbfmvol2  34638  omssubadd  34671  sibfinima  34710  eulerpartlemr  34745  eulerpartlemgf  34750  fiblem  34769  domprobmeas  34781  ballotlemscr  34890  ballotlemfg  34897  ballotlemfrc  34898  ballotlemfrceq  34900  ballotlemrinv0  34904  chtvalz  34997  bnj563  35113  bnj658  35121  bnj667  35122  bnj570  35274  bnj938  35306  bnj1001  35328  bnj1006  35329  bnj1049  35343  bnj1121  35354  bnj1173  35371  bnj1177  35375  bnj1245  35383  bnj1311  35393  bnj1321  35396  bnj1388  35402  bnj1398  35403  bnj1415  35407  bnj1417  35410  bnj1421  35411  bnj1442  35418  bnj1452  35421  bnj1489  35425  bnj1312  35427  pthacycspth  35630  pconntop  35698  sconnpconn  35700  cvmcn  35735  cvmliftlem10  35767  sate0fv0  35890  fundmpss  36240  txpss3v  36349  pprodss4v  36355  outsideofcol  36606  fnebas  36836  filnetlem3  36872  bj-nnfe  37337  bj-xpcossxp  37814  bj-rvecmod  37920  pibt2  38044  phpreu  38236  matunitlindflem1  38248  matunitlindflem2  38249  matunitlindf  38250  poimirlem26  38278  itg2addnc  38306  istotbnd3  38403  totbndmet  38404  sstotbnd2  38406  sstotbnd  38407  equivtotbnd  38410  bndmet  38413  totbndbnd  38421  prdstotbnd  38426  smgrpismgmOLD  38494  mndoissmgrpOLD  38500  crngorngo  38632  prrngorngo  38683  divrngpr  38685  xrnss3v  39011  dfxrn2  39015  refressn  39163  antisymressn  39164  symrelim  39273  eqvrelsym  39319  eqvreltr  39321  disjimeceqim  39434  disjorimxrn  39478  disjim  39514  disjlem14  39531  ollat  39968  omlol  39995  cvlatl  40080  hlomcmcv  40111  2dim  40225  1dimN  40226  lcfl8b  42259  lclkrlem2  42287  lclkrslem1  42292  lclkrslem2  42293  lcfrlem9  42305  mapdval2N  42385  mapdordlem2  42392  mapdrvallem2  42400  idomnnzgmulnz  42881  aks6d1c6lem3  42920  readvrec2  43103  readvrec  43104  readvcot  43106  nacsacs  43423  eldiophelnn0  43478  lnmlmod  43789  lnrring  43822  mncply  43847  idomodle  43901  areaquad  43926  dfno2  44137  harval3  44247  alephiso3  44268  mnurndlem1  44974  nznngen  45009  binomcxplemcvg  45047  2uasbanh  45253  relpf  45642  disjinfi  45893  climxrre  46447  mbfdmssre  46697  stoweidlem14  46711  stoweidlem16  46713  stoweidlem24  46721  stoweidlem51  46748  stoweidlem54  46751  etransclem32  46963  sge0fodjrnlem  47113  pimrecltpos  47405  pimrecltneg  47421  smfaddlem1  47460  smflimsuplem7  47523  ndmafv  47860  dfafv23  47973  dfatcolem  47975  dfatco  47976  evenz  48378  oddz  48379  gbeeven  48502  gbowodd  48503  sclnbgrisvtx  48597  grlimgredgex  48748  idomcanr  49096  ssnn0ssfz  49112  elbigof  49317  digvalnn0  49362  2sphere  49512  mof0  49599  mof0ALT  49601  uobeq2  50162  thincc  50183  termcthin  50238