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

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

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 400

This theorem is referenced by:  an3  669  xoror  1537  just1-df  2085  dfsbimp  2091  euex  2603  reurex  3370  rabidim1  3435  pssss  4051  eldifi  4084  elinel1  4153  ssunsn2  4784  pwssun  5537  sopo  5572  wefr  5635  opelxp1  5687  relop  5820  ssrelrn  5868  ordtr  6356  funmo  6533  funrel  6534  fnfun  6617  ffn  6687  f1f  6756  f1of1  6801  f1ofo  6810  isof1o  7303  eqopi  8002  1st2nd2  8005  reldmtpos  8209  brinxper  8703  swoer  8705  ecopover  8798  sdomdom  8957  mapfien  9351  inf3lemd  9579  cardprclem  9934  infxpenlem  9966  cardinfima  10050  dfac5lem4  10079  dfac5lem4OLD  10081  domtriomlem  10396  smobeth  10541  fpwwe2lem5  10590  fpwwe2lem6  10591  fpwwe2lem11  10596  fpwwe2lem12  10597  fpwwe2  10598  axrnegex  11117  axpre-sup  11124  zre  12569  ixxss1  13364  ixxss2  13365  ixxss12  13366  lbioo  13377  ubioo  13378  iccss2  13418  rge0ssre  13457  elfzuz  13522  0wrd0  14550  01sqrexlem6  15257  rlimf  15511  lo1f  15528  lo1dm  15529  o1f  15539  o1dm  15540  mertenslem2  15898  divalglem9  16418  bitsinv2  16460  bitsf1ocnv  16461  gcdcllem1  16516  coprmproddvdslem  16679  prmnn  16691  prmuz2  16713  phimullem  16797  hashgcdlem  16806  1arith  16946  ramtlecl  17019  0ramcl  17042  firest  17444  acsmre  17667  posprs  18331  tospos  18433  latpos  18453  clatpos  18516  dlatl  18539  pslem  18587  tsrlemax  18601  tsrps  18602  chnwrd  18623  sgrpmgm  18741  mndsgrp  18757  grpmnd  18965  nsgsubg  19182  ghmgrp1  19241  ghmgrp2  19242  gimghm  19287  gagrp  19315  gaset  19316  psgneu  19529  efgredeu  19775  ablgrp  19808  cmnmnd  19820  cyggenod2  19908  cyggrp  19913  dprd2dlem1  20066  dprd2da  20067  ablfac2  20114  simpggrp  20119  ogrpgrp  20148  crngring  20274  dvdsrcl  20393  unitcl  20403  rimrhm  20522  brric2  20535  nzrringOLD  20546  subrgring  20603  subrgrcl  20605  rnghmsubcsetclem1  20660  funcrngcsetcALT  20670  rhmsubcsetclem1  20689  rhmsubcrngclem1  20695  domnnzr  20735  drngring  20765  flddrngd  20770  rng1nfld  20808  srngrhm  20874  ofldfld  20901  ofldlt1  20904  lmimlmhm  21111  lveclmod  21153  2idlelbas  21314  rng2idlsubgsubrng  21318  2idlcpblrng  21321  2idlcpbl  21322  qus1  21324  qusrhm  21326  lpirring  21381  cygznlem1  21598  cygznlem3  21601  ofldchr  21608  lbslinds  21865  assalmod  21892  assaring  21893  gsummatr01lem1  22695  topontop  22953  tpstop  22977  mretopd  23132  neiptoptop  23171  perftop  23196  restfpw  23219  cntop1  23280  cntop2  23281  cnptop1  23282  cnptop2  23283  cnprcl  23285  t1ficld  23367  t0top  23369  t1top  23370  haustop  23371  regtop  23373  nrmtop  23376  cnrmtop  23377  pnrmnrm  23380  cmptop  23435  tgcmp  23441  conndisj  23456  conntop  23457  1stctop  23483  llytop  23512  nllytop  23513  hmeocn  23800  filfbas  23888  ufilfil  23944  flimtop  24005  flimfil  24009  alexsublem  24084  ptcmplem3  24094  tsmsfbas  24168  tsmslem1  24169  tsmsgsum  24179  tsmssubm  24183  tsmsres  24184  tsmsf1o  24185  tsmsmhm  24186  tsmsadd  24187  tsmsxplem1  24193  tsmsxplem2  24194  tsmsxp  24195  tlmtmd  24227  tlmlmod  24229  tlmtrg  24230  tvctlm  24237  ressust  24303  uspreg  24313  ucncn  24324  neipcfilu  24335  cuspusp  24339  metxmet  24374  xmstps  24493  msxms  24494  xmsxmet  24496  msmet  24497  nrgngp  24702  nlmngp  24717  nlmlmod  24718  nlmnrg  24719  nvcnlm  24736  nmoi  24768  nghmrcl1  24772  nghmrcl2  24773  nmhmrcl1  24787  nmhmrcl2  24788  qdensere  24809  xrge0gsumle  24874  xrge0tsms  24875  icopnfcnv  24984  cvsclm  25168  cphsscph  25293  cmetmet  25328  cmsms  25390  hlbn  25405  ovolicc2lem5  25563  mblss  25573  mbff  25667  mbfres  25686  i1fmbf  25717  limcmpt  25925  c1liplem1  26038  c1lip2  26040  fta1glem1  26208  fta1glem2  26209  fta1g  26210  fta1b  26212  idomrootle  26213  ply1pid  26223  aacn  26358  ulmf2  26424  logdmnrp  26683  logdmss  26684  logcnlem2  26685  logcnlem3  26686  logcnlem4  26687  logcnlem5  26688  logcn  26689  dvloglem  26690  logf1o2  26692  efopnlem1  26698  logtayl2  26704  cxpcn  26787  cxpcn3lem  26789  cxpcn3  26790  resqrtcn  26791  atandmneg  26948  atandmcj  26951  cosatan  26963  cosatanne0  26964  birthdaylem1  26993  areacl  27004  cxp2lim  27018  jensenlem2  27029  jensen  27030  sqff1o  27223  mpodvdsmulf1o  27235  dvdsmulf1o  27237  lgsqrlem1  27387  lgsqrlem2  27388  lgsqrlem3  27389  lgsqrlem4  27390  lgseisenlem3  27418  chebbnd1  27513  chtppilim  27516  chpchtlim  27520  chpo1ub  27521  dchrmusumlema  27534  dchrvmasumiflem1  27542  dchrisum0lema  27555  dchrisum0lem2  27559  selberg3lem2  27599  pntrsumo1  27606  selbergsb  27616  pnt2  27654  ltsres  27703  noseponlem  27705  reno  28562  tglineeltr  28777  axcontlem2  29112  axcontlem7  29117  axcontlem8  29118  uhgr0vb  29219  lfuhgr1v0e  29401  fusgrusgr  29469  uvtxisvtx  29536  nbupgruvtxres  29554  cusgrusgr  29566  trliswlk  29842  clwlkiswlk  29920  clwwlkclwwlkn  30178  eupthistrl  30359  frgrusgr  30409  frgrwopreglem5  30469  clwwnonrepclwwnon  30493  ablogrpo  30696  bnnv  31015  hlobn  31037  hcauseq  31334  hlimseqi  31338  hlimveci  31339  shss  31359  sh0  31365  chsh  31373  lnopf  32008  bdopln  32010  hmopf  32023  lnfnf  32033  unopf1o  32065  elunop2  32162  elpjhmop  32334  stcltrlem1  32425  mdslle1i  32466  mdslle2i  32467  2reu2rex1  32628  2reureurex  32629  ssnnssfz  32939  xrge0tsmsd  33214  isarchiofld  33340  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem4  33387  isdrng4  33443  reofld  33490  rearchi  33493  quslsm  33552  ufdidom  33699  mplvrpmga  33803  srafldlvec  33844  extdggt0  33915  fldextid  33917  extdgid  33918  extdgmul  33921  extdg1id  33924  ist0cld  34091  creftop  34104  lmxrge0  34210  qqhrhm  34247  esumpcvgval  34336  dynkin  34425  measssd  34473  elmbfmvol2  34525  omssubadd  34558  sibfinima  34597  eulerpartlemr  34632  eulerpartlemgf  34637  fiblem  34656  domprobmeas  34668  ballotlemscr  34777  ballotlemfg  34784  ballotlemfrc  34785  ballotlemfrceq  34787  ballotlemrinv0  34791  chtvalz  34887  bnj563  35003  bnj658  35011  bnj667  35012  bnj570  35164  bnj938  35196  bnj1001  35218  bnj1006  35219  bnj1049  35233  bnj1121  35244  bnj1173  35261  bnj1177  35265  bnj1245  35273  bnj1311  35283  bnj1321  35286  bnj1388  35292  bnj1398  35293  bnj1415  35297  bnj1417  35300  bnj1421  35301  bnj1442  35308  bnj1452  35311  bnj1489  35315  bnj1312  35317  pthacycspth  35471  pconntop  35539  sconnpconn  35541  cvmcn  35576  cvmliftlem10  35608  sate0fv0  35731  fundmpss  36081  txpss3v  36190  pprodss4v  36196  outsideofcol  36447  fnebas  36668  filnetlem3  36704  bj-nnfe  37170  bj-xpcossxp  37645  bj-rvecmod  37751  pibt2  37875  phpreu  38067  matunitlindflem1  38079  matunitlindflem2  38080  matunitlindf  38081  poimirlem26  38109  itg2addnc  38137  istotbnd3  38234  totbndmet  38235  sstotbnd2  38237  sstotbnd  38238  equivtotbnd  38241  bndmet  38244  totbndbnd  38252  prdstotbnd  38257  smgrpismgmOLD  38325  mndoissmgrpOLD  38331  crngorngo  38463  prrngorngo  38514  divrngpr  38516  xrnss3v  38844  dfxrn2  38848  refressn  38996  antisymressn  38997  symrelim  39106  eqvrelsym  39152  eqvreltr  39154  disjimeceqim  39267  disjorimxrn  39311  disjim  39347  disjlem14  39364  ollat  39801  omlol  39828  cvlatl  39913  hlomcmcv  39944  2dim  40058  1dimN  40059  lcfl8b  42092  lclkrlem2  42120  lclkrslem1  42125  lclkrslem2  42126  lcfrlem9  42138  mapdval2N  42218  mapdordlem2  42225  mapdrvallem2  42233  idomnnzgmulnz  42714  aks6d1c6lem3  42753  readvrec2  42934  readvrec  42935  readvcot  42937  nacsacs  43254  eldiophelnn0  43309  lnmlmod  43620  lnrring  43653  mncply  43678  idomodle  43732  areaquad  43757  dfno2  43968  harval3  44078  alephiso3  44099  mnurndlem1  44821  nznngen  44856  binomcxplemcvg  44894  2uasbanh  45101  relpf  45490  disjinfi  45734  climxrre  46288  mbfdmssre  46538  stoweidlem14  46552  stoweidlem16  46554  stoweidlem24  46562  stoweidlem51  46589  stoweidlem54  46592  etransclem32  46804  sge0fodjrnlem  46954  pimrecltpos  47246  pimrecltneg  47262  smfaddlem1  47301  smflimsuplem7  47364  ndmafv  47698  dfafv23  47811  dfatcolem  47813  dfatco  47814  evenz  48216  oddz  48217  gbeeven  48340  gbowodd  48341  sclnbgrisvtx  48435  grlimgredgex  48586  ssnn0ssfz  48935  elbigof  49140  digvalnn0  49185  2sphere  49335  mof0  49423  mof0ALT  49425  uobeq2  49986  thincc  50007  termcthin  50062