Theorem simplbi 499

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  an3  657  xoror  1515  euex  2575  rabidim1  3324  reurex  3374  eqimss  3982  pssss  4036  eldifi  4067  elinel1  4135  ssunsn2  4766  pwssun  5497  sopo  5533  wefr  5590  opelxp1  5641  relop  5772  ssrelrn  5816  ordtr  6295  funmo  6478  funmoOLD  6479  funrel  6480  fnfun  6564  ffn  6630  f1f  6700  f1of1  6745  f1ofo  6753  isof1o  7226  eqopi  7899  1st2nd2  7902  reldmtpos  8081  swoer  8559  ecopover  8641  sdomdom  8801  mapfien  9211  inf3lemd  9429  cardprclem  9781  infxpenlem  9815  cardinfima  9899  dfac5lem4  9928  domtriomlem  10244  smobeth  10388  fpwwe2lem5  10437  fpwwe2lem6  10438  fpwwe2lem11  10443  fpwwe2lem12  10444  fpwwe2  10445  axrnegex  10964  axpre-sup  10971  zre  12369  ixxss1  13143  ixxss2  13144  ixxss12  13145  lbioo  13156  ubioo  13157  iccss2  13196  rge0ssre  13234  elfzuz  13298  0wrd0  14288  sqrlem6  15004  rlimf  15255  lo1f  15272  lo1dm  15273  o1f  15283  o1dm  15284  mertenslem2  15642  divalglem9  16155  bitsinv2  16195  bitsf1ocnv  16196  gcdcllem1  16251  coprmproddvdslem  16412  prmnn  16424  prmuz2  16446  phimullem  16525  hashgcdlem  16534  1arith  16673  ramtlecl  16746  0ramcl  16769  firest  17188  acsmre  17406  posprs  18079  tospos  18183  latpos  18201  clatpos  18264  dlatl  18287  pslem  18335  tsrlemax  18349  tsrps  18350  sgrpmgm  18425  mndsgrp  18436  grpmnd  18629  nsgsubg  18831  ghmgrp1  18881  ghmgrp2  18882  gimghm  18925  gagrp  18943  gaset  18944  psgneu  19159  efgredeu  19403  ablgrp  19436  cmnmnd  19447  cyggenod2  19530  cyggrp  19535  dprd2dlem1  19689  dprd2da  19690  ablfac2  19737  simpggrp  19742  crngring  19840  dvdsrcl  19936  unitcl  19946  brric2  20034  drngring  20043  subrgring  20072  subrgrcl  20074  srngrhm  20156  lmimlmhm  20371  lveclmod  20413  2idlcpbl  20550  qus1  20551  qusrhm  20553  lpirring  20568  nzrring  20577  domnnzr  20611  fldidomOLD  20622  cygznlem1  20819  cygznlem3  20822  lbslinds  21085  assalmod  21112  assaring  21113  assasca  21114  gsummatr01lem1  21849  topontop  22107  tpstop  22131  mretopd  22288  neiptoptop  22327  perftop  22352  restfpw  22375  cntop1  22436  cntop2  22437  cnptop1  22438  cnptop2  22439  cnprcl  22441  t1ficld  22523  t0top  22525  t1top  22526  haustop  22527  regtop  22529  nrmtop  22532  cnrmtop  22533  pnrmnrm  22536  cmptop  22591  tgcmp  22597  conndisj  22612  conntop  22613  1stctop  22639  llytop  22668  nllytop  22669  hmeocn  22956  filfbas  23044  ufilfil  23100  flimtop  23161  flimfil  23165  alexsublem  23240  ptcmplem3  23250  tsmsfbas  23324  tsmslem1  23325  tsmsgsum  23335  tsmssubm  23339  tsmsres  23340  tsmsf1o  23341  tsmsmhm  23342  tsmsadd  23343  tsmsxplem1  23349  tsmsxplem2  23350  tsmsxp  23351  tlmtmd  23383  tlmlmod  23385  tlmtrg  23386  tvctlm  23393  ressust  23460  uspreg  23471  ucncn  23482  neipcfilu  23493  cuspusp  23497  metxmet  23532  xmstps  23651  msxms  23652  xmsxmet  23654  msmet  23655  nrgngp  23871  nlmngp  23886  nlmlmod  23887  nlmnrg  23888  nvcnlm  23905  nmoi  23937  nghmrcl1  23941  nghmrcl2  23942  nmhmrcl1  23956  nmhmrcl2  23957  qdensere  23978  xrge0gsumle  24041  xrge0tsms  24042  icopnfcnv  24150  cvsclm  24334  cphsscph  24460  cmetmet  24495  cmsms  24557  hlbn  24572  ovolicc2lem5  24730  mblss  24740  mbff  24834  mbfres  24853  i1fmbf  24884  limcmpt  25092  c1liplem1  25205  c1lip2  25207  fta1glem1  25375  fta1glem2  25376  fta1g  25377  fta1b  25379  ply1pid  25389  aacn  25522  ulmf2  25588  logdmnrp  25841  logdmss  25842  logcnlem2  25843  logcnlem3  25844  logcnlem4  25845  logcnlem5  25846  logcn  25847  dvloglem  25848  logf1o2  25850  efopnlem1  25856  logtayl2  25862  cxpcn  25943  cxpcn3lem  25945  cxpcn3  25946  resqrtcn  25947  atandmneg  26101  atandmcj  26104  cosatan  26116  cosatanne0  26117  birthdaylem1  26146  areacl  26157  cxp2lim  26171  jensenlem2  26182  jensen  26183  sqff1o  26376  dvdsmulf1o  26388  lgsqrlem1  26539  lgsqrlem2  26540  lgsqrlem3  26541  lgsqrlem4  26542  lgseisenlem3  26570  chebbnd1  26665  chtppilim  26668  chpchtlim  26672  chpo1ub  26673  dchrmusumlema  26686  dchrvmasumiflem1  26694  dchrisum0lema  26707  dchrisum0lem2  26711  selberg3lem2  26751  pntrsumo1  26758  selbergsb  26768  pnt2  26806  tglineeltr  27037  axcontlem2  27378  axcontlem7  27383  axcontlem8  27384  uhgr0vb  27487  lfuhgr1v0e  27666  fusgrusgr  27734  uvtxisvtx  27801  nbupgruvtxres  27819  cusgrusgr  27831  trliswlk  28110  clwlkiswlk  28187  clwwlkclwwlkn  28439  eupthistrl  28620  frgrusgr  28670  frgrwopreglem5  28730  clwwnonrepclwwnon  28754  ablogrpo  28954  bnnv  29273  hlobn  29295  hcauseq  29592  hlimseqi  29596  hlimveci  29597  shss  29617  sh0  29623  chsh  29631  lnopf  30266  bdopln  30268  hmopf  30281  lnfnf  30291  unopf1o  30323  elunop2  30420  elpjhmop  30592  stcltrlem1  30683  mdslle1i  30724  mdslle2i  30725  2reu2rex1  30874  2reureurex  30875  ssnnssfz  31153  xrge0tsmsd  31362  ogrpgrp  31374  ofldfld  31554  ofldlt1  31557  ofldchr  31558  isarchiofld  31561  reofld  31589  rearchi  31591  quslsm  31638  srafldlvec  31721  rgmoddim  31738  extdggt0  31777  fldextid  31779  extdgmul  31781  extdg1id  31783  ist0cld  31828  creftop  31841  lmxrge0  31947  qqhrhm  31984  esumpcvgval  32091  dynkin  32180  measssd  32228  elmbfmvol2  32279  omssubadd  32312  sibfinima  32351  eulerpartlemr  32386  eulerpartlemgf  32391  fiblem  32410  domprobmeas  32422  ballotlemscr  32530  ballotlemfg  32537  ballotlemfrc  32538  ballotlemfrceq  32540  ballotlemrinv0  32544  chtvalz  32654  bnj563  32768  bnj658  32776  bnj667  32777  bnj570  32930  bnj938  32962  bnj1001  32984  bnj1006  32985  bnj1049  32999  bnj1121  33010  bnj1173  33027  bnj1177  33031  bnj1245  33039  bnj1311  33049  bnj1321  33052  bnj1388  33058  bnj1398  33059  bnj1415  33063  bnj1417  33066  bnj1421  33067  bnj1442  33074  bnj1452  33077  bnj1489  33081  bnj1312  33083  pthacycspth  33164  pconntop  33232  sconnpconn  33234  cvmcn  33269  cvmliftlem10  33301  sate0fv0  33424  fundmpss  33785  sltres  33910  noseponlem  33912  txpss3v  34225  pprodss4v  34231  outsideofcol  34480  fnebas  34578  filnetlem3  34614  bj-nnfe  34958  bj-xpcossxp  35404  bj-rvecmod  35510  pibt2  35632  phpreu  35805  matunitlindflem1  35817  matunitlindflem2  35818  matunitlindf  35819  poimirlem26  35847  itg2addnc  35875  istotbnd3  35973  totbndmet  35974  sstotbnd2  35976  sstotbnd  35977  equivtotbnd  35980  bndmet  35983  totbndbnd  35991  prdstotbnd  35996  smgrpismgmOLD  36064  mndoissmgrpOLD  36070  crngorngo  36202  prrngorngo  36253  divrngpr  36255  xrnss3v  36544  dfxrn2  36548  symrelim  36715  eqvrelsym  36760  eqvreltr  36762  disjorimxrn  36898  ollat  37269  omlol  37296  cvlatl  37381  hlomcmcv  37412  2dim  37526  1dimN  37527  lcfl8b  39560  lclkrlem2  39588  lclkrslem1  39593  lclkrslem2  39594  lcfrlem9  39606  mapdval2N  39686  mapdordlem2  39693  mapdrvallem2  39701  prjcrv0  40507  nacsacs  40568  eldiophelnn0  40623  lnmlmod  40942  lnrring  40975  mncply  41000  idomrootle  41058  idomodle  41059  areaquad  41085  harval3  41183  alephiso3  41204  mnurndlem1  41937  nznngen  41972  binomcxplemcvg  42010  2uasbanh  42219  fompt  42774  disjinfi  42775  climxrre  43340  mbfdmssre  43590  stoweidlem14  43604  stoweidlem16  43606  stoweidlem24  43614  stoweidlem51  43641  stoweidlem54  43644  etransclem32  43856  sge0fodjrnlem  44004  pimrecltpos  44296  pimrecltneg  44312  smfaddlem1  44351  smflimsuplem7  44413  ndmafv  44690  dfafv23  44803  dfatcolem  44805  dfatco  44806  evenz  45140  oddz  45141  gbeeven  45264  gbowodd  45265  rnghmsubcsetclem1  45591  funcrngcsetcALT  45615  rhmsubcsetclem1  45637  rhmsubcrngclem1  45643  ssnn0ssfz  45743  elbigof  45958  digvalnn0  46003  2sphere  46153  mof0  46223  mof0ALT  46225  thincc  46363  upwordisword  46574