Theorem simplbi 500

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 218	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 497	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  an3  657  xoror  1509  sbequ2OLDOLD  2514  sbequ2ALT  2580  euex  2662  rabidim1  3380  reurex  3431  eqimss  4023  pssss  4072  eldifi  4103  elinel1  4172  ssunsn2  4760  pwssun  5456  sopo  5492  wefr  5545  opelxp1  5596  relop  5721  ssrelrn  5763  ordtr  6205  funmo  6371  funrel  6372  fnfun  6453  ffn  6514  f1f  6575  f1of1  6614  f1ofo  6622  isof1o  7076  eqopi  7725  1st2nd2  7728  reldmtpos  7900  swoer  8319  ecopover  8401  sdomdom  8537  mapfien  8871  inf3lemd  9090  cardprclem  9408  infxpenlem  9439  cardinfima  9523  dfac5lem4  9552  domtriomlem  9864  smobeth  10008  fpwwe2lem6  10057  fpwwe2lem7  10058  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  axrnegex  10584  axpre-sup  10591  zre  11986  ixxss1  12757  ixxss2  12758  ixxss12  12759  lbioo  12770  ubioo  12771  iccss2  12808  rge0ssre  12845  elfzuz  12905  0wrd0  13890  sqrlem6  14607  rlimf  14858  lo1f  14875  lo1dm  14876  o1f  14886  o1dm  14887  mertenslem2  15241  divalglem9  15752  bitsinv2  15792  bitsf1ocnv  15793  gcdcllem1  15848  coprmproddvdslem  16006  prmnn  16018  prmuz2  16040  phimullem  16116  hashgcdlem  16125  1arith  16263  ramtlecl  16336  0ramcl  16359  firest  16706  acsmre  16923  posprs  17559  latpos  17660  clatpos  17720  dlatl  17805  pslem  17816  tsrlemax  17830  tsrps  17831  sgrpmgm  17906  mndsgrp  17917  grpmnd  18110  nsgsubg  18310  ghmgrp1  18360  ghmgrp2  18361  gimghm  18404  gagrp  18422  gaset  18423  psgneu  18634  efgredeu  18878  ablgrp  18911  cmnmnd  18922  cyggenod2  19004  cyggrp  19009  dprd2dlem1  19163  dprd2da  19164  ablfac2  19211  simpggrp  19216  crngring  19308  dvdsrcl  19399  unitcl  19409  brric2  19500  drngring  19509  subrgring  19538  subrgrcl  19540  srngrhm  19622  lmimlmhm  19836  lveclmod  19878  2idlcpbl  20007  qus1  20008  qusrhm  20010  lpirring  20025  nzrring  20034  domnnzr  20068  fldidom  20078  assalmod  20092  assaring  20093  assasca  20094  cygznlem1  20713  cygznlem3  20716  lbslinds  20977  gsummatr01lem1  21264  topontop  21521  tpstop  21545  mretopd  21700  neiptoptop  21739  perftop  21764  restfpw  21787  cntop1  21848  cntop2  21849  cnptop1  21850  cnptop2  21851  cnprcl  21853  t1ficld  21935  t0top  21937  t1top  21938  haustop  21939  regtop  21941  nrmtop  21944  cnrmtop  21945  pnrmnrm  21948  cmptop  22003  tgcmp  22009  conndisj  22024  conntop  22025  1stctop  22051  llytop  22080  nllytop  22081  hmeocn  22368  filfbas  22456  ufilfil  22512  flimtop  22573  flimfil  22577  alexsublem  22652  ptcmplem3  22662  tsmsfbas  22736  tsmslem1  22737  tsmsgsum  22747  tsmssubm  22751  tsmsres  22752  tsmsf1o  22753  tsmsmhm  22754  tsmsadd  22755  tsmsxplem1  22761  tsmsxplem2  22762  tsmsxp  22763  tlmtmd  22795  tlmlmod  22797  tlmtrg  22798  tvctlm  22805  ressust  22873  uspreg  22883  ucncn  22894  neipcfilu  22905  cuspusp  22909  metxmet  22944  xmstps  23063  msxms  23064  xmsxmet  23066  msmet  23067  nrgngp  23271  nlmngp  23286  nlmlmod  23287  nlmnrg  23288  nvcnlm  23305  nmoi  23337  nghmrcl1  23341  nghmrcl2  23342  nmhmrcl1  23356  nmhmrcl2  23357  qdensere  23378  xrge0gsumle  23441  xrge0tsms  23442  icopnfcnv  23546  cvsclm  23730  cphsscph  23854  cmetmet  23889  cmsms  23951  hlbn  23966  ovolicc2lem5  24122  mblss  24132  mbff  24226  mbfres  24245  i1fmbf  24276  limcmpt  24481  c1liplem1  24593  c1lip2  24595  fta1glem1  24759  fta1glem2  24760  fta1g  24761  fta1b  24763  ply1pid  24773  aacn  24906  ulmf2  24972  logdmnrp  25224  logdmss  25225  logcnlem2  25226  logcnlem3  25227  logcnlem4  25228  logcnlem5  25229  logcn  25230  dvloglem  25231  logf1o2  25233  efopnlem1  25239  logtayl2  25245  cxpcn  25326  cxpcn3lem  25328  cxpcn3  25329  resqrtcn  25330  atandmneg  25484  atandmcj  25487  cosatan  25499  cosatanne0  25500  birthdaylem1  25529  areacl  25540  cxp2lim  25554  jensenlem2  25565  jensen  25566  sqff1o  25759  dvdsmulf1o  25771  lgsqrlem1  25922  lgsqrlem2  25923  lgsqrlem3  25924  lgsqrlem4  25925  lgseisenlem3  25953  chebbnd1  26048  chtppilim  26051  chpchtlim  26055  chpo1ub  26056  dchrmusumlema  26069  dchrvmasumiflem1  26077  dchrisum0lema  26090  dchrisum0lem2  26094  selberg3lem2  26134  pntrsumo1  26141  selbergsb  26151  pnt2  26189  tglineeltr  26417  axcontlem2  26751  axcontlem7  26756  axcontlem8  26757  uhgr0vb  26857  lfuhgr1v0e  27036  fusgrusgr  27104  uvtxisvtx  27171  nbupgruvtxres  27189  cusgrusgr  27201  trliswlk  27479  clwlkiswlk  27555  clwwlkclwwlkn  27808  eupthistrl  27990  frgrusgr  28040  frgrwopreglem5  28100  clwwnonrepclwwnon  28124  ablogrpo  28324  bnnv  28643  hlobn  28665  hcauseq  28962  hlimseqi  28966  hlimveci  28967  shss  28987  sh0  28993  chsh  29001  lnopf  29636  bdopln  29638  hmopf  29651  lnfnf  29661  unopf1o  29693  elunop2  29790  elpjhmop  29962  stcltrlem1  30053  mdslle1i  30094  mdslle2i  30095  2reu2rex1  30244  2reureurex  30245  ssnnssfz  30510  tospos  30645  xrge0tsmsd  30692  ogrpgrp  30704  ofldfld  30883  ofldlt1  30886  ofldchr  30887  isarchiofld  30890  reofld  30913  rearchi  30915  srafldlvec  30991  rgmoddim  31008  extdggt0  31047  fldextid  31049  extdgmul  31051  extdg1id  31053  creftop  31110  lmxrge0  31195  qqhrhm  31230  esumpcvgval  31337  dynkin  31426  measssd  31474  elmbfmvol2  31525  omssubadd  31558  sibfinima  31597  eulerpartlemr  31632  eulerpartlemgf  31637  fiblem  31656  domprobmeas  31668  ballotlemscr  31776  ballotlemfg  31783  ballotlemfrc  31784  ballotlemfrceq  31786  ballotlemrinv0  31790  chtvalz  31900  bnj563  32014  bnj658  32022  bnj667  32023  bnj570  32177  bnj938  32209  bnj1001  32231  bnj1006  32232  bnj1049  32246  bnj1121  32257  bnj1173  32274  bnj1177  32278  bnj1245  32286  bnj1311  32296  bnj1321  32299  bnj1388  32305  bnj1398  32306  bnj1415  32310  bnj1417  32313  bnj1421  32314  bnj1442  32321  bnj1452  32324  bnj1489  32328  bnj1312  32330  pthacycspth  32404  pconntop  32472  sconnpconn  32474  cvmcn  32509  cvmliftlem10  32541  sate0fv0  32664  fundmpss  33009  sltres  33169  noseponlem  33171  txpss3v  33339  pprodss4v  33345  outsideofcol  33594  fnebas  33692  filnetlem3  33728  bj-nnfe  34062  bj-rvecmod  34579  pibt2  34701  phpreu  34891  matunitlindflem1  34903  matunitlindflem2  34904  matunitlindf  34905  poimirlem26  34933  itg2addnc  34961  istotbnd3  35064  totbndmet  35065  sstotbnd2  35067  sstotbnd  35068  equivtotbnd  35071  bndmet  35074  totbndbnd  35082  prdstotbnd  35087  smgrpismgmOLD  35155  mndoissmgrpOLD  35161  crngorngo  35293  prrngorngo  35344  divrngpr  35346  xrnss3v  35639  dfxrn2  35643  symrelim  35810  eqvrelsym  35855  eqvreltr  35857  disjorimxrn  35993  ollat  36364  omlol  36391  cvlatl  36476  hlomcmcv  36507  2dim  36621  1dimN  36622  lcfl8b  38655  lclkrlem2  38683  lclkrslem1  38688  lclkrslem2  38689  lcfrlem9  38701  mapdval2N  38781  mapdordlem2  38788  mapdrvallem2  38796  nacsacs  39326  eldiophelnn0  39381  lnmlmod  39699  lnrring  39732  mncply  39757  idomrootle  39815  idomodle  39816  areaquad  39843  harval3  39924  alephiso3  39938  mnurndlem1  40637  nznngen  40668  binomcxplemcvg  40706  2uasbanh  40915  fompt  41473  disjinfi  41474  climxrre  42051  mbfdmssre  42305  stoweidlem14  42319  stoweidlem16  42321  stoweidlem24  42329  stoweidlem51  42356  stoweidlem54  42359  etransclem32  42571  sge0fodjrnlem  42718  pimrecltpos  43007  pimrecltneg  43021  smfaddlem1  43059  smflimsuplem7  43120  ndmafv  43359  dfafv23  43472  dfatcolem  43474  dfatco  43475  evenz  43815  oddz  43816  gbeeven  43939  gbowodd  43940  rnghmsubcsetclem1  44266  funcrngcsetcALT  44290  rhmsubcsetclem1  44312  rhmsubcrngclem1  44318  ssnn0ssfz  44417  elbigof  44634  digvalnn0  44679  2sphere  44756