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  2577  reurex  3384  rabidim1  3459  pssss  4098  eldifi  4131  elinel1  4201  ssunsn2  4827  pwssun  5575  sopo  5611  wefr  5675  opelxp1  5727  relop  5861  ssrelrn  5905  ordtr  6398  funmo  6581  funmoOLD  6582  funrel  6583  fnfun  6668  ffn  6736  f1f  6804  f1of1  6847  f1ofo  6855  isof1o  7343  eqopi  8050  1st2nd2  8053  reldmtpos  8259  brinxper  8774  swoer  8776  ecopover  8861  sdomdom  9020  mapfien  9448  inf3lemd  9667  cardprclem  10019  infxpenlem  10053  cardinfima  10137  dfac5lem4  10166  dfac5lem4OLD  10168  domtriomlem  10482  smobeth  10626  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  axrnegex  11202  axpre-sup  11209  zre  12617  ixxss1  13405  ixxss2  13406  ixxss12  13407  lbioo  13418  ubioo  13419  iccss2  13458  rge0ssre  13496  elfzuz  13560  0wrd0  14578  01sqrexlem6  15286  rlimf  15537  lo1f  15554  lo1dm  15555  o1f  15565  o1dm  15566  mertenslem2  15921  divalglem9  16438  bitsinv2  16480  bitsf1ocnv  16481  gcdcllem1  16536  coprmproddvdslem  16699  prmnn  16711  prmuz2  16733  phimullem  16816  hashgcdlem  16825  1arith  16965  ramtlecl  17038  0ramcl  17061  firest  17477  acsmre  17695  posprs  18362  tospos  18465  latpos  18483  clatpos  18546  dlatl  18569  pslem  18617  tsrlemax  18631  tsrps  18632  sgrpmgm  18737  mndsgrp  18753  grpmnd  18958  nsgsubg  19176  ghmgrp1  19236  ghmgrp2  19237  gimghm  19282  gagrp  19310  gaset  19311  psgneu  19524  efgredeu  19770  ablgrp  19803  cmnmnd  19815  cyggenod2  19903  cyggrp  19908  dprd2dlem1  20061  dprd2da  20062  ablfac2  20109  simpggrp  20114  crngring  20242  dvdsrcl  20365  unitcl  20375  rimrhmOLD  20495  rimrhm  20496  brric2  20506  nzrringOLD  20517  subrgring  20574  subrgrcl  20576  rnghmsubcsetclem1  20631  funcrngcsetcALT  20641  rhmsubcsetclem1  20660  rhmsubcrngclem1  20666  domnnzr  20706  drngring  20736  flddrngd  20741  fldidomOLD  20772  rng1nfld  20780  srngrhm  20846  lmimlmhm  21063  lveclmod  21105  2idlelbas  21274  rng2idlsubgsubrng  21278  2idlcpblrng  21281  2idlcpbl  21282  qus1  21284  qusrhm  21286  lpirring  21341  cygznlem1  21585  cygznlem3  21588  lbslinds  21853  assalmod  21880  assaring  21881  gsummatr01lem1  22661  topontop  22919  tpstop  22943  mretopd  23100  neiptoptop  23139  perftop  23164  restfpw  23187  cntop1  23248  cntop2  23249  cnptop1  23250  cnptop2  23251  cnprcl  23253  t1ficld  23335  t0top  23337  t1top  23338  haustop  23339  regtop  23341  nrmtop  23344  cnrmtop  23345  pnrmnrm  23348  cmptop  23403  tgcmp  23409  conndisj  23424  conntop  23425  1stctop  23451  llytop  23480  nllytop  23481  hmeocn  23768  filfbas  23856  ufilfil  23912  flimtop  23973  flimfil  23977  alexsublem  24052  ptcmplem3  24062  tsmsfbas  24136  tsmslem1  24137  tsmsgsum  24147  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  tsmsmhm  24154  tsmsadd  24155  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  tlmtmd  24195  tlmlmod  24197  tlmtrg  24198  tvctlm  24205  ressust  24272  uspreg  24283  ucncn  24294  neipcfilu  24305  cuspusp  24309  metxmet  24344  xmstps  24463  msxms  24464  xmsxmet  24466  msmet  24467  nrgngp  24683  nlmngp  24698  nlmlmod  24699  nlmnrg  24700  nvcnlm  24717  nmoi  24749  nghmrcl1  24753  nghmrcl2  24754  nmhmrcl1  24768  nmhmrcl2  24769  qdensere  24790  xrge0gsumle  24855  xrge0tsms  24856  icopnfcnv  24973  cvsclm  25159  cphsscph  25285  cmetmet  25320  cmsms  25382  hlbn  25397  ovolicc2lem5  25556  mblss  25566  mbff  25660  mbfres  25679  i1fmbf  25710  limcmpt  25918  c1liplem1  26035  c1lip2  26037  fta1glem1  26207  fta1glem2  26208  fta1g  26209  fta1b  26211  idomrootle  26212  ply1pid  26222  aacn  26359  ulmf2  26427  logdmnrp  26683  logdmss  26684  logcnlem2  26685  logcnlem3  26686  logcnlem4  26687  logcnlem5  26688  logcn  26689  dvloglem  26690  logf1o2  26692  efopnlem1  26698  logtayl2  26704  cxpcn  26787  cxpcnOLD  26788  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  atandmneg  26949  atandmcj  26952  cosatan  26964  cosatanne0  26965  birthdaylem1  26994  areacl  27005  cxp2lim  27020  jensenlem2  27031  jensen  27032  sqff1o  27225  mpodvdsmulf1o  27237  dvdsmulf1o  27239  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  lgseisenlem3  27421  chebbnd1  27516  chtppilim  27519  chpchtlim  27523  chpo1ub  27524  dchrmusumlema  27537  dchrvmasumiflem1  27545  dchrisum0lema  27558  dchrisum0lem2  27562  selberg3lem2  27602  pntrsumo1  27609  selbergsb  27619  pnt2  27657  sltres  27707  noseponlem  27709  tglineeltr  28639  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  uhgr0vb  29089  lfuhgr1v0e  29271  fusgrusgr  29339  uvtxisvtx  29406  nbupgruvtxres  29424  cusgrusgr  29436  trliswlk  29715  clwlkiswlk  29794  clwwlkclwwlkn  30049  eupthistrl  30230  frgrusgr  30280  frgrwopreglem5  30340  clwwnonrepclwwnon  30364  ablogrpo  30566  bnnv  30885  hlobn  30907  hcauseq  31204  hlimseqi  31208  hlimveci  31209  shss  31229  sh0  31235  chsh  31243  lnopf  31878  bdopln  31880  hmopf  31893  lnfnf  31903  unopf1o  31935  elunop2  32032  elpjhmop  32204  stcltrlem1  32295  mdslle1i  32336  mdslle2i  32337  2reu2rex1  32500  2reureurex  32501  ssnnssfz  32789  chnwrd  32997  xrge0tsmsd  33065  ogrpgrp  33080  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  isdrng4  33298  ofldfld  33340  ofldlt1  33343  ofldchr  33344  isarchiofld  33347  reofld  33372  rearchi  33374  quslsm  33433  ufdidom  33570  srafldlvec  33637  rgmoddimOLD  33661  extdggt0  33708  fldextid  33710  extdgid  33711  extdgmul  33714  extdg1id  33716  ist0cld  33832  creftop  33845  lmxrge0  33951  qqhrhm  33990  esumpcvgval  34079  dynkin  34168  measssd  34216  elmbfmvol2  34269  omssubadd  34302  sibfinima  34341  eulerpartlemr  34376  eulerpartlemgf  34381  fiblem  34400  domprobmeas  34412  ballotlemscr  34521  ballotlemfg  34528  ballotlemfrc  34529  ballotlemfrceq  34531  ballotlemrinv0  34535  chtvalz  34644  bnj563  34757  bnj658  34765  bnj667  34766  bnj570  34919  bnj938  34951  bnj1001  34973  bnj1006  34974  bnj1049  34988  bnj1121  34999  bnj1173  35016  bnj1177  35020  bnj1245  35028  bnj1311  35038  bnj1321  35041  bnj1388  35047  bnj1398  35048  bnj1415  35052  bnj1417  35055  bnj1421  35056  bnj1442  35063  bnj1452  35066  bnj1489  35070  bnj1312  35072  pthacycspth  35162  pconntop  35230  sconnpconn  35232  cvmcn  35267  cvmliftlem10  35299  sate0fv0  35422  fundmpss  35767  txpss3v  35879  pprodss4v  35885  outsideofcol  36134  fnebas  36345  filnetlem3  36381  bj-nnfe  36732  bj-xpcossxp  37190  bj-rvecmod  37296  pibt2  37418  phpreu  37611  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  poimirlem26  37653  itg2addnc  37681  istotbnd3  37778  totbndmet  37779  sstotbnd2  37781  sstotbnd  37782  equivtotbnd  37785  bndmet  37788  totbndbnd  37796  prdstotbnd  37801  smgrpismgmOLD  37869  mndoissmgrpOLD  37875  crngorngo  38007  prrngorngo  38058  divrngpr  38060  xrnss3v  38373  dfxrn2  38377  refressn  38444  antisymressn  38445  symrelim  38560  eqvrelsym  38606  eqvreltr  38608  disjorimxrn  38749  disjim  38782  disjlem14  38799  ollat  39214  omlol  39241  cvlatl  39326  hlomcmcv  39357  2dim  39472  1dimN  39473  lcfl8b  41506  lclkrlem2  41534  lclkrslem1  41539  lclkrslem2  41540  lcfrlem9  41552  mapdval2N  41632  mapdordlem2  41639  mapdrvallem2  41647  idomnnzgmulnz  42134  aks6d1c6lem3  42173  readvrec2  42391  readvrec  42392  readvcot  42394  nacsacs  42720  eldiophelnn0  42775  lnmlmod  43091  lnrring  43124  mncply  43149  idomodle  43203  areaquad  43228  dfno2  43441  harval3  43551  alephiso3  43572  mnurndlem1  44300  nznngen  44335  binomcxplemcvg  44373  2uasbanh  44581  relpf  44971  disjinfi  45197  climxrre  45765  mbfdmssre  46015  stoweidlem14  46029  stoweidlem16  46031  stoweidlem24  46039  stoweidlem51  46066  stoweidlem54  46069  etransclem32  46281  sge0fodjrnlem  46431  pimrecltpos  46723  pimrecltneg  46739  smfaddlem1  46778  smflimsuplem7  46841  upwordisword  46896  ndmafv  47152  dfafv23  47265  dfatcolem  47267  dfatco  47268  evenz  47617  oddz  47618  gbeeven  47741  gbowodd  47742  sclnbgrisvtx  47835  ssnn0ssfz  48265  elbigof  48475  digvalnn0  48520  2sphere  48670  mof0  48747  mof0ALT  48749  thincc  49072  termcthin  49124