Theorem simplbi 498

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 495	1 ⊢ (𝜑 → 𝜓)

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

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 397

This theorem is referenced by:  an3  657  xoror  1517  euex  2571  reurex  3380  rabidim1  3453  pssss  4095  eldifi  4126  elinel1  4195  ssunsn2  4830  pwssun  5571  sopo  5607  wefr  5666  opelxp1  5718  relop  5850  ssrelrn  5894  ordtr  6378  funmo  6563  funmoOLD  6564  funrel  6565  fnfun  6649  ffn  6717  f1f  6787  f1of1  6832  f1ofo  6840  isof1o  7322  eqopi  8013  1st2nd2  8016  reldmtpos  8221  swoer  8735  ecopover  8817  sdomdom  8978  mapfien  9405  inf3lemd  9624  cardprclem  9976  infxpenlem  10010  cardinfima  10094  dfac5lem4  10123  domtriomlem  10439  smobeth  10583  fpwwe2lem5  10632  fpwwe2lem6  10633  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  axrnegex  11159  axpre-sup  11166  zre  12566  ixxss1  13346  ixxss2  13347  ixxss12  13348  lbioo  13359  ubioo  13360  iccss2  13399  rge0ssre  13437  elfzuz  13501  0wrd0  14494  01sqrexlem6  15198  rlimf  15449  lo1f  15466  lo1dm  15467  o1f  15477  o1dm  15478  mertenslem2  15835  divalglem9  16348  bitsinv2  16388  bitsf1ocnv  16389  gcdcllem1  16444  coprmproddvdslem  16603  prmnn  16615  prmuz2  16637  phimullem  16716  hashgcdlem  16725  1arith  16864  ramtlecl  16937  0ramcl  16960  firest  17382  acsmre  17600  posprs  18273  tospos  18377  latpos  18395  clatpos  18458  dlatl  18481  pslem  18529  tsrlemax  18543  tsrps  18544  sgrpmgm  18649  mndsgrp  18665  grpmnd  18862  nsgsubg  19074  ghmgrp1  19132  ghmgrp2  19133  gimghm  19178  gagrp  19197  gaset  19198  psgneu  19415  efgredeu  19661  ablgrp  19694  cmnmnd  19706  cyggenod2  19794  cyggrp  19799  dprd2dlem1  19952  dprd2da  19953  ablfac2  20000  simpggrp  20005  crngring  20139  dvdsrcl  20256  unitcl  20266  rimrhmOLD  20386  rimrhm  20387  brric2  20397  nzrringOLD  20408  subrgring  20464  subrgrcl  20466  drngring  20507  flddrngd  20512  rng1nfld  20543  srngrhm  20602  lmimlmhm  20819  lveclmod  20861  2idlelbas  21019  2idlcpblrng  21020  2idlcpbl  21021  qus1  21022  qusrhm  21024  rng2idlsubgsubrng  21041  lpirring  21090  domnnzr  21111  fldidomOLD  21124  cygznlem1  21341  cygznlem3  21344  lbslinds  21607  assalmod  21634  assaring  21635  gsummatr01lem1  22377  topontop  22635  tpstop  22659  mretopd  22816  neiptoptop  22855  perftop  22880  restfpw  22903  cntop1  22964  cntop2  22965  cnptop1  22966  cnptop2  22967  cnprcl  22969  t1ficld  23051  t0top  23053  t1top  23054  haustop  23055  regtop  23057  nrmtop  23060  cnrmtop  23061  pnrmnrm  23064  cmptop  23119  tgcmp  23125  conndisj  23140  conntop  23141  1stctop  23167  llytop  23196  nllytop  23197  hmeocn  23484  filfbas  23572  ufilfil  23628  flimtop  23689  flimfil  23693  alexsublem  23768  ptcmplem3  23778  tsmsfbas  23852  tsmslem1  23853  tsmsgsum  23863  tsmssubm  23867  tsmsres  23868  tsmsf1o  23869  tsmsmhm  23870  tsmsadd  23871  tsmsxplem1  23877  tsmsxplem2  23878  tsmsxp  23879  tlmtmd  23911  tlmlmod  23913  tlmtrg  23914  tvctlm  23921  ressust  23988  uspreg  23999  ucncn  24010  neipcfilu  24021  cuspusp  24025  metxmet  24060  xmstps  24179  msxms  24180  xmsxmet  24182  msmet  24183  nrgngp  24399  nlmngp  24414  nlmlmod  24415  nlmnrg  24416  nvcnlm  24433  nmoi  24465  nghmrcl1  24469  nghmrcl2  24470  nmhmrcl1  24484  nmhmrcl2  24485  qdensere  24506  xrge0gsumle  24569  xrge0tsms  24570  icopnfcnv  24682  cvsclm  24866  cphsscph  24992  cmetmet  25027  cmsms  25089  hlbn  25104  ovolicc2lem5  25262  mblss  25272  mbff  25366  mbfres  25385  i1fmbf  25416  limcmpt  25624  c1liplem1  25737  c1lip2  25739  fta1glem1  25907  fta1glem2  25908  fta1g  25909  fta1b  25911  ply1pid  25921  aacn  26054  ulmf2  26120  logdmnrp  26373  logdmss  26374  logcnlem2  26375  logcnlem3  26376  logcnlem4  26377  logcnlem5  26378  logcn  26379  dvloglem  26380  logf1o2  26382  efopnlem1  26388  logtayl2  26394  cxpcn  26477  cxpcn3lem  26479  cxpcn3  26480  resqrtcn  26481  atandmneg  26635  atandmcj  26638  cosatan  26650  cosatanne0  26651  birthdaylem1  26680  areacl  26691  cxp2lim  26705  jensenlem2  26716  jensen  26717  sqff1o  26910  dvdsmulf1o  26922  lgsqrlem1  27073  lgsqrlem2  27074  lgsqrlem3  27075  lgsqrlem4  27076  lgseisenlem3  27104  chebbnd1  27199  chtppilim  27202  chpchtlim  27206  chpo1ub  27207  dchrmusumlema  27220  dchrvmasumiflem1  27228  dchrisum0lema  27241  dchrisum0lem2  27245  selberg3lem2  27285  pntrsumo1  27292  selbergsb  27302  pnt2  27340  sltres  27389  noseponlem  27391  tglineeltr  28137  axcontlem2  28478  axcontlem7  28483  axcontlem8  28484  uhgr0vb  28587  lfuhgr1v0e  28766  fusgrusgr  28834  uvtxisvtx  28901  nbupgruvtxres  28919  cusgrusgr  28931  trliswlk  29209  clwlkiswlk  29286  clwwlkclwwlkn  29538  eupthistrl  29719  frgrusgr  29769  frgrwopreglem5  29829  clwwnonrepclwwnon  29853  ablogrpo  30055  bnnv  30374  hlobn  30396  hcauseq  30693  hlimseqi  30697  hlimveci  30698  shss  30718  sh0  30724  chsh  30732  lnopf  31367  bdopln  31369  hmopf  31382  lnfnf  31392  unopf1o  31424  elunop2  31521  elpjhmop  31693  stcltrlem1  31784  mdslle1i  31825  mdslle2i  31826  2reu2rex1  31976  2reureurex  31977  ssnnssfz  32253  xrge0tsmsd  32467  ogrpgrp  32479  isdrng4  32653  ofldfld  32686  ofldlt1  32689  ofldchr  32690  isarchiofld  32693  reofld  32717  rearchi  32719  quslsm  32778  srafldlvec  32949  rgmoddimOLD  32971  extdggt0  33012  fldextid  33014  extdgid  33015  extdgmul  33016  extdg1id  33018  ist0cld  33099  creftop  33112  lmxrge0  33218  qqhrhm  33255  esumpcvgval  33362  dynkin  33451  measssd  33499  elmbfmvol2  33552  omssubadd  33585  sibfinima  33624  eulerpartlemr  33659  eulerpartlemgf  33664  fiblem  33683  domprobmeas  33695  ballotlemscr  33803  ballotlemfg  33810  ballotlemfrc  33811  ballotlemfrceq  33813  ballotlemrinv0  33817  chtvalz  33927  bnj563  34040  bnj658  34048  bnj667  34049  bnj570  34202  bnj938  34234  bnj1001  34256  bnj1006  34257  bnj1049  34271  bnj1121  34282  bnj1173  34299  bnj1177  34303  bnj1245  34311  bnj1311  34321  bnj1321  34324  bnj1388  34330  bnj1398  34331  bnj1415  34335  bnj1417  34338  bnj1421  34339  bnj1442  34346  bnj1452  34349  bnj1489  34353  bnj1312  34355  pthacycspth  34434  pconntop  34502  sconnpconn  34504  cvmcn  34539  cvmliftlem10  34571  sate0fv0  34694  fundmpss  35030  txpss3v  35142  pprodss4v  35148  outsideofcol  35397  gg-cxpcn  35470  fnebas  35532  filnetlem3  35568  bj-nnfe  35912  bj-xpcossxp  36373  bj-rvecmod  36479  pibt2  36601  phpreu  36775  matunitlindflem1  36787  matunitlindflem2  36788  matunitlindf  36789  poimirlem26  36817  itg2addnc  36845  istotbnd3  36942  totbndmet  36943  sstotbnd2  36945  sstotbnd  36946  equivtotbnd  36949  bndmet  36952  totbndbnd  36960  prdstotbnd  36965  smgrpismgmOLD  37033  mndoissmgrpOLD  37039  crngorngo  37171  prrngorngo  37222  divrngpr  37224  xrnss3v  37545  dfxrn2  37549  refressn  37616  antisymressn  37617  symrelim  37732  eqvrelsym  37778  eqvreltr  37780  disjorimxrn  37921  disjim  37954  disjlem14  37971  ollat  38386  omlol  38413  cvlatl  38498  hlomcmcv  38529  2dim  38644  1dimN  38645  lcfl8b  40678  lclkrlem2  40706  lclkrslem1  40711  lclkrslem2  40712  lcfrlem9  40724  mapdval2N  40804  mapdordlem2  40811  mapdrvallem2  40819  nacsacs  41749  eldiophelnn0  41804  lnmlmod  42123  lnrring  42156  mncply  42181  idomrootle  42239  idomodle  42240  areaquad  42267  dfno2  42481  harval3  42591  alephiso3  42612  mnurndlem1  43342  nznngen  43377  binomcxplemcvg  43415  2uasbanh  43624  disjinfi  44190  climxrre  44765  mbfdmssre  45015  stoweidlem14  45029  stoweidlem16  45031  stoweidlem24  45039  stoweidlem51  45066  stoweidlem54  45069  etransclem32  45281  sge0fodjrnlem  45431  pimrecltpos  45723  pimrecltneg  45739  smfaddlem1  45778  smflimsuplem7  45841  upwordisword  45894  ndmafv  46147  dfafv23  46260  dfatcolem  46262  dfatco  46263  evenz  46597  oddz  46598  gbeeven  46721  gbowodd  46722  rnghmsubcsetclem1  46962  funcrngcsetcALT  46986  rhmsubcsetclem1  47008  rhmsubcrngclem1  47014  ssnn0ssfz  47114  elbigof  47328  digvalnn0  47373  2sphere  47523  mof0  47592  mof0ALT  47594  thincc  47732