Theorem simplbi 502

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an3  672  xoror  1547  euex  2602  reurex  3369  rabidim1  3433  pssss  4025  eldifi  4067  elinel1  4098  ssunsn2  4782  pwssun  5542  sopo  5577  wefr  5640  opelxp1  5692  relop  5827  ssrelrn  5875  ordtr  6376  funmo  6555  funrel  6557  fnfun  6640  ffn  6710  f1f  6779  f1of1  6824  f1ofo  6833  isof1o  7332  eqopi  8038  1st2nd2  8041  reldmtpos  8255  brinxper  8751  swoer  8753  ecopover  8846  sdomdom  9011  mapfien  9404  inf3lemd  9632  cardprclem  10064  infxpenlem  10096  cardinfima  10180  dfac5lem4  10209  domtriomlem  10524  smobeth  10675  fpwwe2lem5  10724  fpwwe2lem6  10725  fpwwe2lem11  10730  fpwwe2lem12  10731  fpwwe2  10732  axrnegex  11251  axpre-sup  11258  zre  12701  ixxss1  13498  ixxss2  13499  ixxss12  13500  lbioo  13511  ubioo  13512  iccss2  13552  rge0ssre  13591  elfzuz  13656  0wrd0  14689  01sqrexlem6  15420  rlimf  15674  lo1f  15691  lo1dm  15692  o1f  15702  o1dm  15703  mertenslem2  16060  divalglem9  16577  bitsinv2  16619  bitsf1ocnv  16620  gcdcllem1  16675  coprmproddvdslem  16843  prmnn  16855  prmuz2  16877  phimullem  16962  hashgcdlem  16971  1arith  17111  ramtlecl  17184  0ramcl  17207  firest  17609  acsmre  17832  posprs  18496  tospos  18598  latpos  18618  clatpos  18681  dlatl  18704  pslem  18752  tsrlemax  18766  tsrps  18767  chnwrd  18788  sgrpmgm  18919  mndsgrp  18935  grpmnd  19157  nsgsubg  19374  ghmgrp1  19438  ghmgrp2  19439  gimghm  19484  gagrp  19512  gaset  19513  psgneu  19726  efgredeu  19972  ablgrp  20005  cmnmnd  20017  cyggenod2  20105  cyggrp  20110  dprd2dlem1  20263  dprd2da  20264  ablfac2  20311  simpggrp  20316  ogrpgrp  20345  crngring  20478  dvdsrcl  20601  unitcl  20611  rimrhm  20737  isbrric2  20759  nzrringOLD  20773  subrgring  20832  subrgrcl  20834  rnghmsubcsetclem1  20889  funcrngcsetcALT  20899  rhmsubcsetclem1  20918  rhmsubcrngclem1  20924  domnnzr  20964  drngring  20993  isdrng4  20998  flddrngd  21000  rng1nfld  21042  srngrhm  21108  ofldfld  21135  ofldlt1  21138  lmimlmhm  21345  lveclmod  21387  2idlelbas  21564  rng2idlsubgsubrng  21568  2idlcpblrng  21571  2idlcpbl  21572  qus1  21574  qusrhm  21576  lpirring  21661  cygznlem1  21878  cygznlem3  21881  ofldchr  21888  lbslinds  22145  assalmod  22174  assaring  22175  gsummatr01lem1  22976  matunitlindflem1  23000  matunitlindflem2  23001  matunitlindf  23002  topontop  23237  tpstop  23261  mretopd  23416  neiptoptop  23455  perftop  23480  restfpw  23503  cntop1  23564  cntop2  23565  cnptop1  23566  cnptop2  23567  cnprcl  23569  t1ficld  23651  t0top  23653  t1top  23654  haustop  23655  regtop  23657  nrmtop  23660  cnrmtop  23661  pnrmnrm  23664  cmptop  23719  tgcmp  23725  conndisj  23740  conntop  23741  1stctop  23767  llytop  23797  nllytop  23798  hmeocn  24085  filfbas  24173  ufilfil  24229  flimtop  24290  flimfil  24294  alexsublem  24369  ptcmplem3  24379  tsmsfbas  24453  tsmslem1  24454  tsmsgsum  24464  tsmssubm  24468  tsmsres  24469  tsmsf1o  24470  tsmsmhm  24471  tsmsadd  24472  tsmsxplem1  24478  tsmsxplem2  24479  tsmsxp  24480  tlmtmd  24512  tlmlmod  24514  tlmtrg  24515  tvctlm  24522  ressust  24588  uspreg  24598  ucncn  24609  neipcfilu  24620  cuspusp  24624  metxmet  24659  xmstps  24778  msxms  24779  xmsxmet  24781  msmet  24782  nrgngp  24987  nlmngp  25002  nlmlmod  25003  nlmnrg  25004  nvcnlm  25021  nmoi  25053  nghmrcl1  25057  nghmrcl2  25058  nmhmrcl1  25072  nmhmrcl2  25073  qdensere  25094  xrge0gsumle  25159  xrge0tsms  25160  icopnfcnv  25269  cvsclm  25453  cphsscph  25578  cmetmet  25613  cmsms  25675  hlbn  25690  ovolicc2lem5  25848  mblss  25858  mbff  25952  mbfres  25971  i1fmbf  26002  limcmpt  26209  c1liplem1  26322  c1lip2  26324  fta1glem1  26492  fta1glem2  26493  fta1g  26494  fta1b  26496  idomrootle  26497  ply1pid  26507  aacn  26646  ulmf2  26717  logdmnrp  26975  logdmss  26976  logcnlem2  26977  logcnlem3  26978  logcnlem4  26979  logcnlem5  26980  logcn  26981  dvloglem  26982  logf1o2  26984  efopnlem1  26990  logtayl2  26996  cxpcn  27079  cxpcn3lem  27081  cxpcn3  27082  resqrtcn  27083  atandmneg  27240  atandmcj  27243  cosatan  27255  cosatanne0  27256  birthdaylem1  27285  areacl  27296  cxp2lim  27310  jensenlem2  27321  jensen  27322  sqff1o  27515  mpodvdsmulf1o  27527  dvdsmulf1o  27529  lgsqrlem1  27679  lgsqrlem2  27680  lgsqrlem3  27681  lgsqrlem4  27682  lgseisenlem3  27710  chebbnd1  27805  chtppilim  27808  chpchtlim  27812  chpo1ub  27813  dchrmusumlema  27826  dchrvmasumiflem1  27834  dchrisum0lema  27847  dchrisum0lem2  27851  selberg3lem2  27891  pntrsumo1  27898  selbergsb  27908  pnt2  27946  ltsres  28025  noseponlem  28027  reno  28884  tglineeltr  29105  axcontlem2  29549  axcontlem7  29554  axcontlem8  29555  uhgr0vb  29656  lfuhgr1v0e  29841  fusgrusgr  29909  uvtxisvtx  29976  nbupgruvtxres  29994  cusgrusgr  30006  trliswlk  30286  clwlkiswlk  30367  clwwlkclwwlkn  30627  eupthistrl  30818  frgrusgr  30868  frgrwopreglem5  30928  clwwnonrepclwwnon  30952  ablogrpo  31155  bnnv  31474  hlobn  31496  hcauseq  31793  hlimseqi  31797  hlimveci  31798  shss  31818  sh0  31824  chsh  31832  lnopf  32467  bdopln  32469  hmopf  32482  lnfnf  32492  unopf1o  32524  elunop2  32621  elpjhmop  32793  stcltrlem1  32884  mdslle1i  32925  mdslle2i  32926  2reu2rex1  33125  2reureurex  33126  ssnnssfz  33426  xrge0tsmsd  33681  isarchiofld  33807  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem4  33853  reofld  33951  rearchi  33954  quslsm  34003  ufdidom  34121  mplvrpmga  34224  srafldlvec  34265  extdggt0  34336  fldextid  34338  extdgid  34339  extdgmul  34342  extdg1id  34345  ist0cld  34512  creftop  34525  lmxrge0  34631  qqhrhm  34668  esumpcvgval  34757  dynkin  34847  measssd  34895  elmbfmvol2  34946  sibfinima  35018  eulerpartlemr  35053  eulerpartlemgf  35058  fiblem  35077  domprobmeas  35089  ballotlemscr  35198  ballotlemfg  35205  ballotlemfrc  35206  ballotlemfrceq  35208  ballotlemrinv0  35212  chtvalz  35305  bnj563  35421  bnj658  35429  bnj667  35430  bnj570  35582  bnj938  35614  bnj1001  35636  bnj1006  35637  bnj1049  35651  bnj1121  35662  bnj1173  35679  bnj1177  35683  bnj1245  35691  bnj1311  35701  bnj1321  35704  bnj1388  35710  bnj1398  35711  bnj1415  35715  bnj1417  35718  bnj1421  35719  bnj1442  35726  bnj1452  35729  bnj1489  35733  bnj1312  35735  fwfffunres  35765  pthacycspth  35999  pconntop  36077  sconnpconn  36079  cvmcn  36114  cvmliftlem10  36146  sate0fv0  36269  fundmpss  36625  txpss3v  36733  pprodss4v  36739  outsideofcol  36991  fnebas  37225  filnetlem3  37261  bj-nnfe  37726  bj-xpcossxp  38204  bj-rvecmod  38310  pibt2  38434  phpreu  38621  poimirlem26  38658  itg2addnc  38686  istotbnd3  38799  totbndmet  38800  sstotbnd2  38802  sstotbnd  38803  equivtotbnd  38806  bndmet  38809  totbndbnd  38817  prdstotbnd  38822  smgrpismgmOLD  38890  mndoissmgrpOLD  38896  crngorngo  39028  prrngorngo  39079  divrngpr  39081  xrnss3v  39407  dfxrn2  39411  refressn  39559  antisymressn  39560  symrelim  39669  eqvrelsym  39715  eqvreltr  39717  disjimeceqim  39830  disjorimxrn  39874  disjim  39910  disjlem14  39927  ollat  40364  omlol  40391  cvlatl  40476  hlomcmcv  40507  2dim  40621  1dimN  40622  lcfl8b  42655  lclkrlem2  42683  lclkrslem1  42688  lclkrslem2  42689  lcfrlem9  42701  mapdval2N  42781  mapdordlem2  42788  mapdrvallem2  42796  idomnnzgmulnz  43277  aks6d1c6lem3  43316  readvrec2  43506  readvrec  43507  readvcot  43509  nacsacs  43814  eldiophelnn0  43869  lnmlmod  44175  lnrring  44208  mncply  44233  idomodle  44287  areaquad  44312  dfno2  44523  harval3  44633  alephiso3  44654  mnurndlem1  45359  nznngen  45394  binomcxplemcvg  45432  2uasbanh  45638  relpf  46034  disjinfi  46301  climxrre  46854  mbfdmssre  47104  stoweidlem14  47118  stoweidlem16  47120  stoweidlem24  47128  stoweidlem51  47155  stoweidlem54  47158  etransclem32  47370  sge0fodjrnlem  47520  pimrecltpos  47812  pimrecltneg  47828  smfaddlem1  47867  smflimsuplem7  47930  chnrin  48000  ndmafv  48304  dfafv23  48417  dfatcolem  48419  dfatco  48420  evenz  48822  oddz  48823  gbeeven  48946  gbowodd  48947  sclnbgrisvtx  49041  grlimgredgex  49192  idomcanr  49539  ssnn0ssfz  49555  elbigof  49760  digvalnn0  49805  2sphere  49955  mof0  50043  mof0ALT  50045  uobeq2  50630  thinccat  50651  termcthin  50706