Theorem simplbi 502

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  659  xoror  1511  euex  2597  rabidim1  3299  reurex  3342  eqimss  3949  pssss  4002  eldifi  4033  elinel1  4101  ssunsn2  4718  pwssun  5427  sopo  5462  wefr  5515  opelxp1  5566  relop  5691  ssrelrn  5735  ordtr  6184  funmo  6352  funrel  6353  fnfun  6435  ffn  6499  f1f  6561  f1of1  6602  f1ofo  6610  isof1o  7071  eqopi  7730  1st2nd2  7733  reldmtpos  7911  swoer  8330  ecopover  8412  sdomdom  8556  mapfien  8906  inf3lemd  9124  cardprclem  9442  infxpenlem  9474  cardinfima  9558  dfac5lem4  9587  domtriomlem  9903  smobeth  10047  fpwwe2lem5  10096  fpwwe2lem6  10097  fpwwe2lem11  10102  fpwwe2lem12  10103  fpwwe2  10104  axrnegex  10623  axpre-sup  10630  zre  12025  ixxss1  12798  ixxss2  12799  ixxss12  12800  lbioo  12811  ubioo  12812  iccss2  12851  rge0ssre  12889  elfzuz  12953  0wrd0  13940  sqrlem6  14656  rlimf  14907  lo1f  14924  lo1dm  14925  o1f  14935  o1dm  14936  mertenslem2  15290  divalglem9  15803  bitsinv2  15843  bitsf1ocnv  15844  gcdcllem1  15899  coprmproddvdslem  16059  prmnn  16071  prmuz2  16093  phimullem  16172  hashgcdlem  16181  1arith  16319  ramtlecl  16392  0ramcl  16415  firest  16765  acsmre  16982  posprs  17626  latpos  17727  clatpos  17787  dlatl  17872  pslem  17883  tsrlemax  17897  tsrps  17898  sgrpmgm  17973  mndsgrp  17984  grpmnd  18177  nsgsubg  18378  ghmgrp1  18428  ghmgrp2  18429  gimghm  18472  gagrp  18490  gaset  18491  psgneu  18702  efgredeu  18946  ablgrp  18979  cmnmnd  18990  cyggenod2  19073  cyggrp  19078  dprd2dlem1  19232  dprd2da  19233  ablfac2  19280  simpggrp  19285  crngring  19378  dvdsrcl  19471  unitcl  19481  brric2  19569  drngring  19578  subrgring  19607  subrgrcl  19609  srngrhm  19691  lmimlmhm  19905  lveclmod  19947  2idlcpbl  20076  qus1  20077  qusrhm  20079  lpirring  20094  nzrring  20103  domnnzr  20137  fldidom  20147  cygznlem1  20335  cygznlem3  20338  lbslinds  20599  assalmod  20626  assaring  20627  assasca  20628  gsummatr01lem1  21356  topontop  21614  tpstop  21638  mretopd  21793  neiptoptop  21832  perftop  21857  restfpw  21880  cntop1  21941  cntop2  21942  cnptop1  21943  cnptop2  21944  cnprcl  21946  t1ficld  22028  t0top  22030  t1top  22031  haustop  22032  regtop  22034  nrmtop  22037  cnrmtop  22038  pnrmnrm  22041  cmptop  22096  tgcmp  22102  conndisj  22117  conntop  22118  1stctop  22144  llytop  22173  nllytop  22174  hmeocn  22461  filfbas  22549  ufilfil  22605  flimtop  22666  flimfil  22670  alexsublem  22745  ptcmplem3  22755  tsmsfbas  22829  tsmslem1  22830  tsmsgsum  22840  tsmssubm  22844  tsmsres  22845  tsmsf1o  22846  tsmsmhm  22847  tsmsadd  22848  tsmsxplem1  22854  tsmsxplem2  22855  tsmsxp  22856  tlmtmd  22888  tlmlmod  22890  tlmtrg  22891  tvctlm  22898  ressust  22966  uspreg  22976  ucncn  22987  neipcfilu  22998  cuspusp  23002  metxmet  23037  xmstps  23156  msxms  23157  xmsxmet  23159  msmet  23160  nrgngp  23365  nlmngp  23380  nlmlmod  23381  nlmnrg  23382  nvcnlm  23399  nmoi  23431  nghmrcl1  23435  nghmrcl2  23436  nmhmrcl1  23450  nmhmrcl2  23451  qdensere  23472  xrge0gsumle  23535  xrge0tsms  23536  icopnfcnv  23644  cvsclm  23828  cphsscph  23952  cmetmet  23987  cmsms  24049  hlbn  24064  ovolicc2lem5  24222  mblss  24232  mbff  24326  mbfres  24345  i1fmbf  24376  limcmpt  24583  c1liplem1  24696  c1lip2  24698  fta1glem1  24866  fta1glem2  24867  fta1g  24868  fta1b  24870  ply1pid  24880  aacn  25013  ulmf2  25079  logdmnrp  25332  logdmss  25333  logcnlem2  25334  logcnlem3  25335  logcnlem4  25336  logcnlem5  25337  logcn  25338  dvloglem  25339  logf1o2  25341  efopnlem1  25347  logtayl2  25353  cxpcn  25434  cxpcn3lem  25436  cxpcn3  25437  resqrtcn  25438  atandmneg  25592  atandmcj  25595  cosatan  25607  cosatanne0  25608  birthdaylem1  25637  areacl  25648  cxp2lim  25662  jensenlem2  25673  jensen  25674  sqff1o  25867  dvdsmulf1o  25879  lgsqrlem1  26030  lgsqrlem2  26031  lgsqrlem3  26032  lgsqrlem4  26033  lgseisenlem3  26061  chebbnd1  26156  chtppilim  26159  chpchtlim  26163  chpo1ub  26164  dchrmusumlema  26177  dchrvmasumiflem1  26185  dchrisum0lema  26198  dchrisum0lem2  26202  selberg3lem2  26242  pntrsumo1  26249  selbergsb  26259  pnt2  26297  tglineeltr  26525  axcontlem2  26859  axcontlem7  26864  axcontlem8  26865  uhgr0vb  26965  lfuhgr1v0e  27144  fusgrusgr  27212  uvtxisvtx  27279  nbupgruvtxres  27297  cusgrusgr  27309  trliswlk  27587  clwlkiswlk  27663  clwwlkclwwlkn  27915  eupthistrl  28096  frgrusgr  28146  frgrwopreglem5  28206  clwwnonrepclwwnon  28230  ablogrpo  28430  bnnv  28749  hlobn  28771  hcauseq  29068  hlimseqi  29072  hlimveci  29073  shss  29093  sh0  29099  chsh  29107  lnopf  29742  bdopln  29744  hmopf  29757  lnfnf  29767  unopf1o  29799  elunop2  29896  elpjhmop  30068  stcltrlem1  30159  mdslle1i  30200  mdslle2i  30201  2reu2rex1  30351  2reureurex  30352  ssnnssfz  30633  tospos  30768  xrge0tsmsd  30844  ogrpgrp  30856  ofldfld  31036  ofldlt1  31039  ofldchr  31040  isarchiofld  31043  reofld  31066  rearchi  31068  quslsm  31115  srafldlvec  31198  rgmoddim  31215  extdggt0  31254  fldextid  31256  extdgmul  31258  extdg1id  31260  ist0cld  31305  creftop  31318  lmxrge0  31424  qqhrhm  31459  esumpcvgval  31566  dynkin  31655  measssd  31703  elmbfmvol2  31754  omssubadd  31787  sibfinima  31826  eulerpartlemr  31861  eulerpartlemgf  31866  fiblem  31885  domprobmeas  31897  ballotlemscr  32005  ballotlemfg  32012  ballotlemfrc  32013  ballotlemfrceq  32015  ballotlemrinv0  32019  chtvalz  32129  bnj563  32243  bnj658  32251  bnj667  32252  bnj570  32406  bnj938  32438  bnj1001  32460  bnj1006  32461  bnj1049  32475  bnj1121  32486  bnj1173  32503  bnj1177  32507  bnj1245  32515  bnj1311  32525  bnj1321  32528  bnj1388  32534  bnj1398  32535  bnj1415  32539  bnj1417  32542  bnj1421  32543  bnj1442  32550  bnj1452  32553  bnj1489  32557  bnj1312  32559  pthacycspth  32636  pconntop  32704  sconnpconn  32706  cvmcn  32741  cvmliftlem10  32773  sate0fv0  32896  fundmpss  33257  sltres  33431  noseponlem  33433  txpss3v  33730  pprodss4v  33736  outsideofcol  33985  fnebas  34083  filnetlem3  34119  bj-nnfe  34459  bj-xpcossxp  34885  bj-rvecmod  34990  pibt2  35115  phpreu  35322  matunitlindflem1  35334  matunitlindflem2  35335  matunitlindf  35336  poimirlem26  35364  itg2addnc  35392  istotbnd3  35490  totbndmet  35491  sstotbnd2  35493  sstotbnd  35494  equivtotbnd  35497  bndmet  35500  totbndbnd  35508  prdstotbnd  35513  smgrpismgmOLD  35581  mndoissmgrpOLD  35587  crngorngo  35719  prrngorngo  35770  divrngpr  35772  xrnss3v  36065  dfxrn2  36069  symrelim  36236  eqvrelsym  36281  eqvreltr  36283  disjorimxrn  36419  ollat  36790  omlol  36817  cvlatl  36902  hlomcmcv  36933  2dim  37047  1dimN  37048  lcfl8b  39081  lclkrlem2  39109  lclkrslem1  39114  lclkrslem2  39115  lcfrlem9  39127  mapdval2N  39207  mapdordlem2  39214  mapdrvallem2  39222  nacsacs  40024  eldiophelnn0  40079  lnmlmod  40397  lnrring  40430  mncply  40455  idomrootle  40513  idomodle  40514  areaquad  40540  harval3  40618  alephiso3  40632  mnurndlem1  41363  nznngen  41394  binomcxplemcvg  41432  2uasbanh  41641  fompt  42190  disjinfi  42191  climxrre  42759  mbfdmssre  43009  stoweidlem14  43023  stoweidlem16  43025  stoweidlem24  43033  stoweidlem51  43060  stoweidlem54  43063  etransclem32  43275  sge0fodjrnlem  43422  pimrecltpos  43711  pimrecltneg  43725  smfaddlem1  43763  smflimsuplem7  43824  ndmafv  44065  dfafv23  44178  dfatcolem  44180  dfatco  44181  evenz  44516  oddz  44517  gbeeven  44640  gbowodd  44641  rnghmsubcsetclem1  44967  funcrngcsetcALT  44991  rhmsubcsetclem1  45013  rhmsubcrngclem1  45019  ssnn0ssfz  45119  elbigof  45334  digvalnn0  45379  2sphere  45529