Theorem simplbi 497

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an3  659  xoror  1518  euex  2576  reurex  3363  rabidim1  3438  pssss  4073  eldifi  4106  elinel1  4176  ssunsn2  4803  pwssun  5545  sopo  5580  wefr  5644  opelxp1  5696  relop  5830  ssrelrn  5874  ordtr  6366  funmo  6550  funmoOLD  6551  funrel  6552  fnfun  6637  ffn  6705  f1f  6773  f1of1  6816  f1ofo  6824  isof1o  7315  eqopi  8022  1st2nd2  8025  reldmtpos  8231  brinxper  8746  swoer  8748  ecopover  8833  sdomdom  8992  mapfien  9418  inf3lemd  9639  cardprclem  9991  infxpenlem  10025  cardinfima  10109  dfac5lem4  10138  dfac5lem4OLD  10140  domtriomlem  10454  smobeth  10598  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  axrnegex  11174  axpre-sup  11181  zre  12590  ixxss1  13378  ixxss2  13379  ixxss12  13380  lbioo  13391  ubioo  13392  iccss2  13432  rge0ssre  13471  elfzuz  13535  0wrd0  14556  01sqrexlem6  15264  rlimf  15515  lo1f  15532  lo1dm  15533  o1f  15543  o1dm  15544  mertenslem2  15899  divalglem9  16418  bitsinv2  16460  bitsf1ocnv  16461  gcdcllem1  16516  coprmproddvdslem  16679  prmnn  16691  prmuz2  16713  phimullem  16796  hashgcdlem  16805  1arith  16945  ramtlecl  17018  0ramcl  17041  firest  17444  acsmre  17662  posprs  18326  tospos  18428  latpos  18446  clatpos  18509  dlatl  18532  pslem  18580  tsrlemax  18594  tsrps  18595  sgrpmgm  18700  mndsgrp  18716  grpmnd  18921  nsgsubg  19139  ghmgrp1  19199  ghmgrp2  19200  gimghm  19245  gagrp  19273  gaset  19274  psgneu  19485  efgredeu  19731  ablgrp  19764  cmnmnd  19776  cyggenod2  19864  cyggrp  19869  dprd2dlem1  20022  dprd2da  20023  ablfac2  20070  simpggrp  20075  crngring  20203  dvdsrcl  20323  unitcl  20333  rimrhmOLD  20453  rimrhm  20454  brric2  20464  nzrringOLD  20475  subrgring  20532  subrgrcl  20534  rnghmsubcsetclem1  20589  funcrngcsetcALT  20599  rhmsubcsetclem1  20618  rhmsubcrngclem1  20624  domnnzr  20664  drngring  20694  flddrngd  20699  rng1nfld  20737  srngrhm  20803  lmimlmhm  21020  lveclmod  21062  2idlelbas  21223  rng2idlsubgsubrng  21227  2idlcpblrng  21230  2idlcpbl  21231  qus1  21233  qusrhm  21235  lpirring  21290  cygznlem1  21525  cygznlem3  21528  lbslinds  21791  assalmod  21818  assaring  21819  gsummatr01lem1  22591  topontop  22849  tpstop  22873  mretopd  23028  neiptoptop  23067  perftop  23092  restfpw  23115  cntop1  23176  cntop2  23177  cnptop1  23178  cnptop2  23179  cnprcl  23181  t1ficld  23263  t0top  23265  t1top  23266  haustop  23267  regtop  23269  nrmtop  23272  cnrmtop  23273  pnrmnrm  23276  cmptop  23331  tgcmp  23337  conndisj  23352  conntop  23353  1stctop  23379  llytop  23408  nllytop  23409  hmeocn  23696  filfbas  23784  ufilfil  23840  flimtop  23901  flimfil  23905  alexsublem  23980  ptcmplem3  23990  tsmsfbas  24064  tsmslem1  24065  tsmsgsum  24075  tsmssubm  24079  tsmsres  24080  tsmsf1o  24081  tsmsmhm  24082  tsmsadd  24083  tsmsxplem1  24089  tsmsxplem2  24090  tsmsxp  24091  tlmtmd  24123  tlmlmod  24125  tlmtrg  24126  tvctlm  24133  ressust  24200  uspreg  24210  ucncn  24221  neipcfilu  24232  cuspusp  24236  metxmet  24271  xmstps  24390  msxms  24391  xmsxmet  24393  msmet  24394  nrgngp  24599  nlmngp  24614  nlmlmod  24615  nlmnrg  24616  nvcnlm  24633  nmoi  24665  nghmrcl1  24669  nghmrcl2  24670  nmhmrcl1  24684  nmhmrcl2  24685  qdensere  24706  xrge0gsumle  24771  xrge0tsms  24772  icopnfcnv  24889  cvsclm  25075  cphsscph  25201  cmetmet  25236  cmsms  25298  hlbn  25313  ovolicc2lem5  25472  mblss  25482  mbff  25576  mbfres  25595  i1fmbf  25626  limcmpt  25834  c1liplem1  25951  c1lip2  25953  fta1glem1  26123  fta1glem2  26124  fta1g  26125  fta1b  26127  idomrootle  26128  ply1pid  26138  aacn  26275  ulmf2  26343  logdmnrp  26600  logdmss  26601  logcnlem2  26602  logcnlem3  26603  logcnlem4  26604  logcnlem5  26605  logcn  26606  dvloglem  26607  logf1o2  26609  efopnlem1  26615  logtayl2  26621  cxpcn  26704  cxpcnOLD  26705  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  atandmneg  26866  atandmcj  26869  cosatan  26881  cosatanne0  26882  birthdaylem1  26911  areacl  26922  cxp2lim  26937  jensenlem2  26948  jensen  26949  sqff1o  27142  mpodvdsmulf1o  27154  dvdsmulf1o  27156  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  lgseisenlem3  27338  chebbnd1  27433  chtppilim  27436  chpchtlim  27440  chpo1ub  27441  dchrmusumlema  27454  dchrvmasumiflem1  27462  dchrisum0lema  27475  dchrisum0lem2  27479  selberg3lem2  27519  pntrsumo1  27526  selbergsb  27536  pnt2  27574  sltres  27624  noseponlem  27626  tglineeltr  28556  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  uhgr0vb  28997  lfuhgr1v0e  29179  fusgrusgr  29247  uvtxisvtx  29314  nbupgruvtxres  29332  cusgrusgr  29344  trliswlk  29623  clwlkiswlk  29702  clwwlkclwwlkn  29957  eupthistrl  30138  frgrusgr  30188  frgrwopreglem5  30248  clwwnonrepclwwnon  30272  ablogrpo  30474  bnnv  30793  hlobn  30815  hcauseq  31112  hlimseqi  31116  hlimveci  31117  shss  31137  sh0  31143  chsh  31151  lnopf  31786  bdopln  31788  hmopf  31801  lnfnf  31811  unopf1o  31843  elunop2  31940  elpjhmop  32112  stcltrlem1  32203  mdslle1i  32244  mdslle2i  32245  2reu2rex1  32408  2reureurex  32409  ssnnssfz  32710  chnwrd  32933  xrge0tsmsd  33002  ogrpgrp  33017  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  isdrng4  33235  ofldfld  33278  ofldlt1  33281  ofldchr  33282  isarchiofld  33285  reofld  33305  rearchi  33307  quslsm  33366  ufdidom  33503  srafldlvec  33572  rgmoddimOLD  33596  extdggt0  33645  fldextid  33647  extdgid  33648  extdgmul  33651  extdg1id  33653  ist0cld  33810  creftop  33823  lmxrge0  33929  qqhrhm  33966  esumpcvgval  34055  dynkin  34144  measssd  34192  elmbfmvol2  34245  omssubadd  34278  sibfinima  34317  eulerpartlemr  34352  eulerpartlemgf  34357  fiblem  34376  domprobmeas  34388  ballotlemscr  34497  ballotlemfg  34504  ballotlemfrc  34505  ballotlemfrceq  34507  ballotlemrinv0  34511  chtvalz  34607  bnj563  34720  bnj658  34728  bnj667  34729  bnj570  34882  bnj938  34914  bnj1001  34936  bnj1006  34937  bnj1049  34951  bnj1121  34962  bnj1173  34979  bnj1177  34983  bnj1245  34991  bnj1311  35001  bnj1321  35004  bnj1388  35010  bnj1398  35011  bnj1415  35015  bnj1417  35018  bnj1421  35019  bnj1442  35026  bnj1452  35029  bnj1489  35033  bnj1312  35035  pthacycspth  35125  pconntop  35193  sconnpconn  35195  cvmcn  35230  cvmliftlem10  35262  sate0fv0  35385  fundmpss  35730  txpss3v  35842  pprodss4v  35848  outsideofcol  36097  fnebas  36308  filnetlem3  36344  bj-nnfe  36695  bj-xpcossxp  37153  bj-rvecmod  37259  pibt2  37381  phpreu  37574  matunitlindflem1  37586  matunitlindflem2  37587  matunitlindf  37588  poimirlem26  37616  itg2addnc  37644  istotbnd3  37741  totbndmet  37742  sstotbnd2  37744  sstotbnd  37745  equivtotbnd  37748  bndmet  37751  totbndbnd  37759  prdstotbnd  37764  smgrpismgmOLD  37832  mndoissmgrpOLD  37838  crngorngo  37970  prrngorngo  38021  divrngpr  38023  xrnss3v  38336  dfxrn2  38340  refressn  38407  antisymressn  38408  symrelim  38523  eqvrelsym  38569  eqvreltr  38571  disjorimxrn  38712  disjim  38745  disjlem14  38762  ollat  39177  omlol  39204  cvlatl  39289  hlomcmcv  39320  2dim  39435  1dimN  39436  lcfl8b  41469  lclkrlem2  41497  lclkrslem1  41502  lclkrslem2  41503  lcfrlem9  41515  mapdval2N  41595  mapdordlem2  41602  mapdrvallem2  41610  idomnnzgmulnz  42092  aks6d1c6lem3  42131  readvrec2  42351  readvrec  42352  readvcot  42354  nacsacs  42679  eldiophelnn0  42734  lnmlmod  43050  lnrring  43083  mncply  43108  idomodle  43162  areaquad  43187  dfno2  43399  harval3  43509  alephiso3  43530  mnurndlem1  44253  nznngen  44288  binomcxplemcvg  44326  2uasbanh  44534  relpf  44923  disjinfi  45164  climxrre  45727  mbfdmssre  45977  stoweidlem14  45991  stoweidlem16  45993  stoweidlem24  46001  stoweidlem51  46028  stoweidlem54  46031  etransclem32  46243  sge0fodjrnlem  46393  pimrecltpos  46685  pimrecltneg  46701  smfaddlem1  46740  smflimsuplem7  46803  upwordisword  46858  ndmafv  47117  dfafv23  47230  dfatcolem  47232  dfatco  47233  evenz  47592  oddz  47593  gbeeven  47716  gbowodd  47717  sclnbgrisvtx  47810  ssnn0ssfz  48272  elbigof  48482  digvalnn0  48527  2sphere  48677  mof0  48764  mof0ALT  48766  thincc  49256  termcthin  49311