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  1519  euex  2577  reurex  3354  rabidim1  3421  pssss  4050  eldifi  4083  elinel1  4153  ssunsn2  4783  pwssun  5516  sopo  5551  wefr  5614  opelxp1  5666  relop  5799  ssrelrn  5843  ordtr  6331  funmo  6508  funrel  6509  fnfun  6592  ffn  6662  f1f  6730  f1of1  6773  f1ofo  6781  isof1o  7269  eqopi  7969  1st2nd2  7972  reldmtpos  8176  brinxper  8664  swoer  8666  ecopover  8758  sdomdom  8917  mapfien  9311  inf3lemd  9536  cardprclem  9891  infxpenlem  9923  cardinfima  10007  dfac5lem4  10036  dfac5lem4OLD  10038  domtriomlem  10352  smobeth  10497  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  axrnegex  11073  axpre-sup  11080  zre  12492  ixxss1  13279  ixxss2  13280  ixxss12  13281  lbioo  13292  ubioo  13293  iccss2  13333  rge0ssre  13372  elfzuz  13436  0wrd0  14463  01sqrexlem6  15170  rlimf  15424  lo1f  15441  lo1dm  15442  o1f  15452  o1dm  15453  mertenslem2  15808  divalglem9  16328  bitsinv2  16370  bitsf1ocnv  16371  gcdcllem1  16426  coprmproddvdslem  16589  prmnn  16601  prmuz2  16623  phimullem  16706  hashgcdlem  16715  1arith  16855  ramtlecl  16928  0ramcl  16951  firest  17352  acsmre  17575  posprs  18239  tospos  18341  latpos  18361  clatpos  18424  dlatl  18447  pslem  18495  tsrlemax  18509  tsrps  18510  chnwrd  18531  sgrpmgm  18649  mndsgrp  18665  grpmnd  18870  nsgsubg  19087  ghmgrp1  19147  ghmgrp2  19148  gimghm  19193  gagrp  19221  gaset  19222  psgneu  19435  efgredeu  19681  ablgrp  19714  cmnmnd  19726  cyggenod2  19814  cyggrp  19819  dprd2dlem1  19972  dprd2da  19973  ablfac2  20020  simpggrp  20025  ogrpgrp  20054  crngring  20180  dvdsrcl  20301  unitcl  20311  rimrhm  20429  brric2  20439  nzrringOLD  20450  subrgring  20507  subrgrcl  20509  rnghmsubcsetclem1  20564  funcrngcsetcALT  20574  rhmsubcsetclem1  20593  rhmsubcrngclem1  20599  domnnzr  20639  drngring  20669  flddrngd  20674  rng1nfld  20712  srngrhm  20778  ofldfld  20805  ofldlt1  20808  lmimlmhm  21016  lveclmod  21058  2idlelbas  21219  rng2idlsubgsubrng  21223  2idlcpblrng  21226  2idlcpbl  21227  qus1  21229  qusrhm  21231  lpirring  21286  cygznlem1  21521  cygznlem3  21524  ofldchr  21531  lbslinds  21788  assalmod  21815  assaring  21816  gsummatr01lem1  22599  topontop  22857  tpstop  22881  mretopd  23036  neiptoptop  23075  perftop  23100  restfpw  23123  cntop1  23184  cntop2  23185  cnptop1  23186  cnptop2  23187  cnprcl  23189  t1ficld  23271  t0top  23273  t1top  23274  haustop  23275  regtop  23277  nrmtop  23280  cnrmtop  23281  pnrmnrm  23284  cmptop  23339  tgcmp  23345  conndisj  23360  conntop  23361  1stctop  23387  llytop  23416  nllytop  23417  hmeocn  23704  filfbas  23792  ufilfil  23848  flimtop  23909  flimfil  23913  alexsublem  23988  ptcmplem3  23998  tsmsfbas  24072  tsmslem1  24073  tsmsgsum  24083  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  tsmsmhm  24090  tsmsadd  24091  tsmsxplem1  24097  tsmsxplem2  24098  tsmsxp  24099  tlmtmd  24131  tlmlmod  24133  tlmtrg  24134  tvctlm  24141  ressust  24207  uspreg  24217  ucncn  24228  neipcfilu  24239  cuspusp  24243  metxmet  24278  xmstps  24397  msxms  24398  xmsxmet  24400  msmet  24401  nrgngp  24606  nlmngp  24621  nlmlmod  24622  nlmnrg  24623  nvcnlm  24640  nmoi  24672  nghmrcl1  24676  nghmrcl2  24677  nmhmrcl1  24691  nmhmrcl2  24692  qdensere  24713  xrge0gsumle  24778  xrge0tsms  24779  icopnfcnv  24896  cvsclm  25082  cphsscph  25207  cmetmet  25242  cmsms  25304  hlbn  25319  ovolicc2lem5  25478  mblss  25488  mbff  25582  mbfres  25601  i1fmbf  25632  limcmpt  25840  c1liplem1  25957  c1lip2  25959  fta1glem1  26129  fta1glem2  26130  fta1g  26131  fta1b  26133  idomrootle  26134  ply1pid  26144  aacn  26281  ulmf2  26349  logdmnrp  26606  logdmss  26607  logcnlem2  26608  logcnlem3  26609  logcnlem4  26610  logcnlem5  26611  logcn  26612  dvloglem  26613  logf1o2  26615  efopnlem1  26621  logtayl2  26627  cxpcn  26710  cxpcnOLD  26711  cxpcn3lem  26713  cxpcn3  26714  resqrtcn  26715  atandmneg  26872  atandmcj  26875  cosatan  26887  cosatanne0  26888  birthdaylem1  26917  areacl  26928  cxp2lim  26943  jensenlem2  26954  jensen  26955  sqff1o  27148  mpodvdsmulf1o  27160  dvdsmulf1o  27162  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  lgseisenlem3  27344  chebbnd1  27439  chtppilim  27442  chpchtlim  27446  chpo1ub  27447  dchrmusumlema  27460  dchrvmasumiflem1  27468  dchrisum0lema  27481  dchrisum0lem2  27485  selberg3lem2  27525  pntrsumo1  27532  selbergsb  27542  pnt2  27580  ltsres  27630  noseponlem  27632  reno  28488  tglineeltr  28703  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  uhgr0vb  29145  lfuhgr1v0e  29327  fusgrusgr  29395  uvtxisvtx  29462  nbupgruvtxres  29480  cusgrusgr  29492  trliswlk  29769  clwlkiswlk  29847  clwwlkclwwlkn  30105  eupthistrl  30286  frgrusgr  30336  frgrwopreglem5  30396  clwwnonrepclwwnon  30420  ablogrpo  30622  bnnv  30941  hlobn  30963  hcauseq  31260  hlimseqi  31264  hlimveci  31265  shss  31285  sh0  31291  chsh  31299  lnopf  31934  bdopln  31936  hmopf  31949  lnfnf  31959  unopf1o  31991  elunop2  32088  elpjhmop  32260  stcltrlem1  32351  mdslle1i  32392  mdslle2i  32393  2reu2rex1  32555  2reureurex  32556  ssnnssfz  32867  xrge0tsmsd  33155  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  isdrng4  33377  reofld  33424  rearchi  33427  quslsm  33486  ufdidom  33623  mplvrpmga  33710  srafldlvec  33742  rgmoddimOLD  33767  extdggt0  33814  fldextid  33816  extdgid  33817  extdgmul  33820  extdg1id  33823  ist0cld  33990  creftop  34003  lmxrge0  34109  qqhrhm  34146  esumpcvgval  34235  dynkin  34324  measssd  34372  elmbfmvol2  34424  omssubadd  34457  sibfinima  34496  eulerpartlemr  34531  eulerpartlemgf  34536  fiblem  34555  domprobmeas  34567  ballotlemscr  34676  ballotlemfg  34683  ballotlemfrc  34684  ballotlemfrceq  34686  ballotlemrinv0  34690  chtvalz  34786  bnj563  34899  bnj658  34907  bnj667  34908  bnj570  35061  bnj938  35093  bnj1001  35115  bnj1006  35116  bnj1049  35130  bnj1121  35141  bnj1173  35158  bnj1177  35162  bnj1245  35170  bnj1311  35180  bnj1321  35183  bnj1388  35189  bnj1398  35190  bnj1415  35194  bnj1417  35197  bnj1421  35198  bnj1442  35205  bnj1452  35208  bnj1489  35212  bnj1312  35214  pthacycspth  35351  pconntop  35419  sconnpconn  35421  cvmcn  35456  cvmliftlem10  35488  sate0fv0  35611  fundmpss  35961  txpss3v  36070  pprodss4v  36076  outsideofcol  36327  fnebas  36538  filnetlem3  36574  bj-nnfe  36932  bj-xpcossxp  37394  bj-rvecmod  37500  pibt2  37622  phpreu  37805  matunitlindflem1  37817  matunitlindflem2  37818  matunitlindf  37819  poimirlem26  37847  itg2addnc  37875  istotbnd3  37972  totbndmet  37973  sstotbnd2  37975  sstotbnd  37976  equivtotbnd  37979  bndmet  37982  totbndbnd  37990  prdstotbnd  37995  smgrpismgmOLD  38063  mndoissmgrpOLD  38069  crngorngo  38201  prrngorngo  38252  divrngpr  38254  xrnss3v  38566  dfxrn2  38570  refressn  38706  antisymressn  38707  symrelim  38816  eqvrelsym  38862  eqvreltr  38864  disjorimxrn  39007  disjim  39040  disjlem14  39057  ollat  39473  omlol  39500  cvlatl  39585  hlomcmcv  39616  2dim  39730  1dimN  39731  lcfl8b  41764  lclkrlem2  41792  lclkrslem1  41797  lclkrslem2  41798  lcfrlem9  41810  mapdval2N  41890  mapdordlem2  41897  mapdrvallem2  41905  idomnnzgmulnz  42387  aks6d1c6lem3  42426  readvrec2  42616  readvrec  42617  readvcot  42619  nacsacs  42951  eldiophelnn0  43006  lnmlmod  43321  lnrring  43354  mncply  43379  idomodle  43433  areaquad  43458  dfno2  43669  harval3  43779  alephiso3  43800  mnurndlem1  44522  nznngen  44557  binomcxplemcvg  44595  2uasbanh  44802  relpf  45191  disjinfi  45436  climxrre  45994  mbfdmssre  46244  stoweidlem14  46258  stoweidlem16  46260  stoweidlem24  46268  stoweidlem51  46295  stoweidlem54  46298  etransclem32  46510  sge0fodjrnlem  46660  pimrecltpos  46952  pimrecltneg  46968  smfaddlem1  47007  smflimsuplem7  47070  ndmafv  47386  dfafv23  47499  dfatcolem  47501  dfatco  47502  evenz  47876  oddz  47877  gbeeven  48000  gbowodd  48001  sclnbgrisvtx  48095  grlimgredgex  48246  ssnn0ssfz  48595  elbigof  48800  digvalnn0  48845  2sphere  48995  mof0  49083  mof0ALT  49085  uobeq2  49646  thincc  49667  termcthin  49722