Theorem simplbi 496

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  660  xoror  1520  euex  2578  reurex  3356  rabidim1  3423  pssss  4052  eldifi  4085  elinel1  4155  ssunsn2  4785  pwssun  5524  sopo  5559  wefr  5622  opelxp1  5674  relop  5807  ssrelrn  5851  ordtr  6339  funmo  6516  funrel  6517  fnfun  6600  ffn  6670  f1f  6738  f1of1  6781  f1ofo  6789  isof1o  7279  eqopi  7979  1st2nd2  7982  reldmtpos  8186  brinxper  8675  swoer  8677  ecopover  8770  sdomdom  8929  mapfien  9323  inf3lemd  9548  cardprclem  9903  infxpenlem  9935  cardinfima  10019  dfac5lem4  10048  dfac5lem4OLD  10050  domtriomlem  10364  smobeth  10509  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  axrnegex  11085  axpre-sup  11092  zre  12504  ixxss1  13291  ixxss2  13292  ixxss12  13293  lbioo  13304  ubioo  13305  iccss2  13345  rge0ssre  13384  elfzuz  13448  0wrd0  14475  01sqrexlem6  15182  rlimf  15436  lo1f  15453  lo1dm  15454  o1f  15464  o1dm  15465  mertenslem2  15820  divalglem9  16340  bitsinv2  16382  bitsf1ocnv  16383  gcdcllem1  16438  coprmproddvdslem  16601  prmnn  16613  prmuz2  16635  phimullem  16718  hashgcdlem  16727  1arith  16867  ramtlecl  16940  0ramcl  16963  firest  17364  acsmre  17587  posprs  18251  tospos  18353  latpos  18373  clatpos  18436  dlatl  18459  pslem  18507  tsrlemax  18521  tsrps  18522  chnwrd  18543  sgrpmgm  18661  mndsgrp  18677  grpmnd  18882  nsgsubg  19099  ghmgrp1  19159  ghmgrp2  19160  gimghm  19205  gagrp  19233  gaset  19234  psgneu  19447  efgredeu  19693  ablgrp  19726  cmnmnd  19738  cyggenod2  19826  cyggrp  19831  dprd2dlem1  19984  dprd2da  19985  ablfac2  20032  simpggrp  20037  ogrpgrp  20066  crngring  20192  dvdsrcl  20313  unitcl  20323  rimrhm  20441  brric2  20451  nzrringOLD  20462  subrgring  20519  subrgrcl  20521  rnghmsubcsetclem1  20576  funcrngcsetcALT  20586  rhmsubcsetclem1  20605  rhmsubcrngclem1  20611  domnnzr  20651  drngring  20681  flddrngd  20686  rng1nfld  20724  srngrhm  20790  ofldfld  20817  ofldlt1  20820  lmimlmhm  21028  lveclmod  21070  2idlelbas  21231  rng2idlsubgsubrng  21235  2idlcpblrng  21238  2idlcpbl  21239  qus1  21241  qusrhm  21243  lpirring  21298  cygznlem1  21533  cygznlem3  21536  ofldchr  21543  lbslinds  21800  assalmod  21827  assaring  21828  gsummatr01lem1  22611  topontop  22869  tpstop  22893  mretopd  23048  neiptoptop  23087  perftop  23112  restfpw  23135  cntop1  23196  cntop2  23197  cnptop1  23198  cnptop2  23199  cnprcl  23201  t1ficld  23283  t0top  23285  t1top  23286  haustop  23287  regtop  23289  nrmtop  23292  cnrmtop  23293  pnrmnrm  23296  cmptop  23351  tgcmp  23357  conndisj  23372  conntop  23373  1stctop  23399  llytop  23428  nllytop  23429  hmeocn  23716  filfbas  23804  ufilfil  23860  flimtop  23921  flimfil  23925  alexsublem  24000  ptcmplem3  24010  tsmsfbas  24084  tsmslem1  24085  tsmsgsum  24095  tsmssubm  24099  tsmsres  24100  tsmsf1o  24101  tsmsmhm  24102  tsmsadd  24103  tsmsxplem1  24109  tsmsxplem2  24110  tsmsxp  24111  tlmtmd  24143  tlmlmod  24145  tlmtrg  24146  tvctlm  24153  ressust  24219  uspreg  24229  ucncn  24240  neipcfilu  24251  cuspusp  24255  metxmet  24290  xmstps  24409  msxms  24410  xmsxmet  24412  msmet  24413  nrgngp  24618  nlmngp  24633  nlmlmod  24634  nlmnrg  24635  nvcnlm  24652  nmoi  24684  nghmrcl1  24688  nghmrcl2  24689  nmhmrcl1  24703  nmhmrcl2  24704  qdensere  24725  xrge0gsumle  24790  xrge0tsms  24791  icopnfcnv  24908  cvsclm  25094  cphsscph  25219  cmetmet  25254  cmsms  25316  hlbn  25331  ovolicc2lem5  25490  mblss  25500  mbff  25594  mbfres  25613  i1fmbf  25644  limcmpt  25852  c1liplem1  25969  c1lip2  25971  fta1glem1  26141  fta1glem2  26142  fta1g  26143  fta1b  26145  idomrootle  26146  ply1pid  26156  aacn  26293  ulmf2  26361  logdmnrp  26618  logdmss  26619  logcnlem2  26620  logcnlem3  26621  logcnlem4  26622  logcnlem5  26623  logcn  26624  dvloglem  26625  logf1o2  26627  efopnlem1  26633  logtayl2  26639  cxpcn  26722  cxpcnOLD  26723  cxpcn3lem  26725  cxpcn3  26726  resqrtcn  26727  atandmneg  26884  atandmcj  26887  cosatan  26899  cosatanne0  26900  birthdaylem1  26929  areacl  26940  cxp2lim  26955  jensenlem2  26966  jensen  26967  sqff1o  27160  mpodvdsmulf1o  27172  dvdsmulf1o  27174  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  lgseisenlem3  27356  chebbnd1  27451  chtppilim  27454  chpchtlim  27458  chpo1ub  27459  dchrmusumlema  27472  dchrvmasumiflem1  27480  dchrisum0lema  27493  dchrisum0lem2  27497  selberg3lem2  27537  pntrsumo1  27544  selbergsb  27554  pnt2  27592  ltsres  27642  noseponlem  27644  reno  28500  tglineeltr  28715  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  uhgr0vb  29157  lfuhgr1v0e  29339  fusgrusgr  29407  uvtxisvtx  29474  nbupgruvtxres  29492  cusgrusgr  29504  trliswlk  29781  clwlkiswlk  29859  clwwlkclwwlkn  30117  eupthistrl  30298  frgrusgr  30348  frgrwopreglem5  30408  clwwnonrepclwwnon  30432  ablogrpo  30634  bnnv  30953  hlobn  30975  hcauseq  31272  hlimseqi  31276  hlimveci  31277  shss  31297  sh0  31303  chsh  31311  lnopf  31946  bdopln  31948  hmopf  31961  lnfnf  31971  unopf1o  32003  elunop2  32100  elpjhmop  32272  stcltrlem1  32363  mdslle1i  32404  mdslle2i  32405  2reu2rex1  32566  2reureurex  32567  ssnnssfz  32877  xrge0tsmsd  33166  isarchiofld  33292  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  isdrng4  33388  reofld  33435  rearchi  33438  quslsm  33497  ufdidom  33634  mplvrpmga  33721  srafldlvec  33762  rgmoddimOLD  33787  extdggt0  33834  fldextid  33836  extdgid  33837  extdgmul  33840  extdg1id  33843  ist0cld  34010  creftop  34023  lmxrge0  34129  qqhrhm  34166  esumpcvgval  34255  dynkin  34344  measssd  34392  elmbfmvol2  34444  omssubadd  34477  sibfinima  34516  eulerpartlemr  34551  eulerpartlemgf  34556  fiblem  34575  domprobmeas  34587  ballotlemscr  34696  ballotlemfg  34703  ballotlemfrc  34704  ballotlemfrceq  34706  ballotlemrinv0  34710  chtvalz  34806  bnj563  34919  bnj658  34927  bnj667  34928  bnj570  35080  bnj938  35112  bnj1001  35134  bnj1006  35135  bnj1049  35149  bnj1121  35160  bnj1173  35177  bnj1177  35181  bnj1245  35189  bnj1311  35199  bnj1321  35202  bnj1388  35208  bnj1398  35209  bnj1415  35213  bnj1417  35216  bnj1421  35217  bnj1442  35224  bnj1452  35227  bnj1489  35231  bnj1312  35233  pthacycspth  35370  pconntop  35438  sconnpconn  35440  cvmcn  35475  cvmliftlem10  35507  sate0fv0  35630  fundmpss  35980  txpss3v  36089  pprodss4v  36095  outsideofcol  36346  fnebas  36557  filnetlem3  36593  bj-nnfe  36971  bj-xpcossxp  37441  bj-rvecmod  37547  pibt2  37669  phpreu  37852  matunitlindflem1  37864  matunitlindflem2  37865  matunitlindf  37866  poimirlem26  37894  itg2addnc  37922  istotbnd3  38019  totbndmet  38020  sstotbnd2  38022  sstotbnd  38023  equivtotbnd  38026  bndmet  38029  totbndbnd  38037  prdstotbnd  38042  smgrpismgmOLD  38110  mndoissmgrpOLD  38116  crngorngo  38248  prrngorngo  38299  divrngpr  38301  xrnss3v  38629  dfxrn2  38633  refressn  38781  antisymressn  38782  symrelim  38891  eqvrelsym  38937  eqvreltr  38939  disjimeceqim  39052  disjorimxrn  39096  disjim  39132  disjlem14  39149  ollat  39586  omlol  39613  cvlatl  39698  hlomcmcv  39729  2dim  39843  1dimN  39844  lcfl8b  41877  lclkrlem2  41905  lclkrslem1  41910  lclkrslem2  41911  lcfrlem9  41923  mapdval2N  42003  mapdordlem2  42010  mapdrvallem2  42018  idomnnzgmulnz  42500  aks6d1c6lem3  42539  readvrec2  42728  readvrec  42729  readvcot  42731  nacsacs  43063  eldiophelnn0  43118  lnmlmod  43433  lnrring  43466  mncply  43491  idomodle  43545  areaquad  43570  dfno2  43781  harval3  43891  alephiso3  43912  mnurndlem1  44634  nznngen  44669  binomcxplemcvg  44707  2uasbanh  44914  relpf  45303  disjinfi  45548  climxrre  46105  mbfdmssre  46355  stoweidlem14  46369  stoweidlem16  46371  stoweidlem24  46379  stoweidlem51  46406  stoweidlem54  46409  etransclem32  46621  sge0fodjrnlem  46771  pimrecltpos  47063  pimrecltneg  47079  smfaddlem1  47118  smflimsuplem7  47181  ndmafv  47497  dfafv23  47610  dfatcolem  47612  dfatco  47613  evenz  47987  oddz  47988  gbeeven  48111  gbowodd  48112  sclnbgrisvtx  48206  grlimgredgex  48357  ssnn0ssfz  48706  elbigof  48911  digvalnn0  48956  2sphere  49106  mof0  49194  mof0ALT  49196  uobeq2  49757  thincc  49778  termcthin  49833