Theorem simplbi 498

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  an3  657  xoror  1517  euex  2570  reurex  3355  rabidim1  3426  pssss  4060  eldifi  4091  elinel1  4160  ssunsn2  4792  pwssun  5533  sopo  5569  wefr  5628  opelxp1  5679  relop  5811  ssrelrn  5855  ordtr  6336  funmo  6521  funmoOLD  6522  funrel  6523  fnfun  6607  ffn  6673  f1f  6743  f1of1  6788  f1ofo  6796  isof1o  7273  eqopi  7962  1st2nd2  7965  reldmtpos  8170  swoer  8685  ecopover  8767  sdomdom  8927  mapfien  9353  inf3lemd  9572  cardprclem  9924  infxpenlem  9958  cardinfima  10042  dfac5lem4  10071  domtriomlem  10387  smobeth  10531  fpwwe2lem5  10580  fpwwe2lem6  10581  fpwwe2lem11  10586  fpwwe2lem12  10587  fpwwe2  10588  axrnegex  11107  axpre-sup  11114  zre  12512  ixxss1  13292  ixxss2  13293  ixxss12  13294  lbioo  13305  ubioo  13306  iccss2  13345  rge0ssre  13383  elfzuz  13447  0wrd0  14440  01sqrexlem6  15144  rlimf  15395  lo1f  15412  lo1dm  15413  o1f  15423  o1dm  15424  mertenslem2  15781  divalglem9  16294  bitsinv2  16334  bitsf1ocnv  16335  gcdcllem1  16390  coprmproddvdslem  16549  prmnn  16561  prmuz2  16583  phimullem  16662  hashgcdlem  16671  1arith  16810  ramtlecl  16883  0ramcl  16906  firest  17328  acsmre  17546  posprs  18219  tospos  18323  latpos  18341  clatpos  18404  dlatl  18427  pslem  18475  tsrlemax  18489  tsrps  18490  sgrpmgm  18565  mndsgrp  18576  grpmnd  18769  nsgsubg  18974  ghmgrp1  19024  ghmgrp2  19025  gimghm  19068  gagrp  19086  gaset  19087  psgneu  19302  efgredeu  19548  ablgrp  19581  cmnmnd  19593  cyggenod2  19676  cyggrp  19681  dprd2dlem1  19834  dprd2da  19835  ablfac2  19882  simpggrp  19887  crngring  19990  dvdsrcl  20092  unitcl  20102  rimrhmOLD  20184  rimrhm  20185  brric2  20195  nzrringOLD  20206  drngring  20232  rng1nfld  20265  subrgring  20273  subrgrcl  20275  srngrhm  20366  lmimlmhm  20582  lveclmod  20624  2idlcpbl  20763  qus1  20764  qusrhm  20766  lpirring  20781  domnnzr  20802  fldidomOLD  20813  cygznlem1  21010  cygznlem3  21013  lbslinds  21276  assalmod  21303  assaring  21304  gsummatr01lem1  22041  topontop  22299  tpstop  22323  mretopd  22480  neiptoptop  22519  perftop  22544  restfpw  22567  cntop1  22628  cntop2  22629  cnptop1  22630  cnptop2  22631  cnprcl  22633  t1ficld  22715  t0top  22717  t1top  22718  haustop  22719  regtop  22721  nrmtop  22724  cnrmtop  22725  pnrmnrm  22728  cmptop  22783  tgcmp  22789  conndisj  22804  conntop  22805  1stctop  22831  llytop  22860  nllytop  22861  hmeocn  23148  filfbas  23236  ufilfil  23292  flimtop  23353  flimfil  23357  alexsublem  23432  ptcmplem3  23442  tsmsfbas  23516  tsmslem1  23517  tsmsgsum  23527  tsmssubm  23531  tsmsres  23532  tsmsf1o  23533  tsmsmhm  23534  tsmsadd  23535  tsmsxplem1  23541  tsmsxplem2  23542  tsmsxp  23543  tlmtmd  23575  tlmlmod  23577  tlmtrg  23578  tvctlm  23585  ressust  23652  uspreg  23663  ucncn  23674  neipcfilu  23685  cuspusp  23689  metxmet  23724  xmstps  23843  msxms  23844  xmsxmet  23846  msmet  23847  nrgngp  24063  nlmngp  24078  nlmlmod  24079  nlmnrg  24080  nvcnlm  24097  nmoi  24129  nghmrcl1  24133  nghmrcl2  24134  nmhmrcl1  24148  nmhmrcl2  24149  qdensere  24170  xrge0gsumle  24233  xrge0tsms  24234  icopnfcnv  24342  cvsclm  24526  cphsscph  24652  cmetmet  24687  cmsms  24749  hlbn  24764  ovolicc2lem5  24922  mblss  24932  mbff  25026  mbfres  25045  i1fmbf  25076  limcmpt  25284  c1liplem1  25397  c1lip2  25399  fta1glem1  25567  fta1glem2  25568  fta1g  25569  fta1b  25571  ply1pid  25581  aacn  25714  ulmf2  25780  logdmnrp  26033  logdmss  26034  logcnlem2  26035  logcnlem3  26036  logcnlem4  26037  logcnlem5  26038  logcn  26039  dvloglem  26040  logf1o2  26042  efopnlem1  26048  logtayl2  26054  cxpcn  26135  cxpcn3lem  26137  cxpcn3  26138  resqrtcn  26139  atandmneg  26293  atandmcj  26296  cosatan  26308  cosatanne0  26309  birthdaylem1  26338  areacl  26349  cxp2lim  26363  jensenlem2  26374  jensen  26375  sqff1o  26568  dvdsmulf1o  26580  lgsqrlem1  26731  lgsqrlem2  26732  lgsqrlem3  26733  lgsqrlem4  26734  lgseisenlem3  26762  chebbnd1  26857  chtppilim  26860  chpchtlim  26864  chpo1ub  26865  dchrmusumlema  26878  dchrvmasumiflem1  26886  dchrisum0lema  26899  dchrisum0lem2  26903  selberg3lem2  26943  pntrsumo1  26950  selbergsb  26960  pnt2  26998  sltres  27047  noseponlem  27049  tglineeltr  27636  axcontlem2  27977  axcontlem7  27982  axcontlem8  27983  uhgr0vb  28086  lfuhgr1v0e  28265  fusgrusgr  28333  uvtxisvtx  28400  nbupgruvtxres  28418  cusgrusgr  28430  trliswlk  28708  clwlkiswlk  28785  clwwlkclwwlkn  29037  eupthistrl  29218  frgrusgr  29268  frgrwopreglem5  29328  clwwnonrepclwwnon  29352  ablogrpo  29552  bnnv  29871  hlobn  29893  hcauseq  30190  hlimseqi  30194  hlimveci  30195  shss  30215  sh0  30221  chsh  30229  lnopf  30864  bdopln  30866  hmopf  30879  lnfnf  30889  unopf1o  30921  elunop2  31018  elpjhmop  31190  stcltrlem1  31281  mdslle1i  31322  mdslle2i  31323  2reu2rex1  31473  2reureurex  31474  ssnnssfz  31758  xrge0tsmsd  31969  ogrpgrp  31981  ofldfld  32176  ofldlt1  32179  ofldchr  32180  isarchiofld  32183  reofld  32207  rearchi  32209  quslsm  32260  srafldlvec  32374  rgmoddim  32392  extdggt0  32433  fldextid  32435  extdgmul  32437  extdg1id  32439  ist0cld  32503  creftop  32516  lmxrge0  32622  qqhrhm  32659  esumpcvgval  32766  dynkin  32855  measssd  32903  elmbfmvol2  32956  omssubadd  32989  sibfinima  33028  eulerpartlemr  33063  eulerpartlemgf  33068  fiblem  33087  domprobmeas  33099  ballotlemscr  33207  ballotlemfg  33214  ballotlemfrc  33215  ballotlemfrceq  33217  ballotlemrinv0  33221  chtvalz  33331  bnj563  33444  bnj658  33452  bnj667  33453  bnj570  33606  bnj938  33638  bnj1001  33660  bnj1006  33661  bnj1049  33675  bnj1121  33686  bnj1173  33703  bnj1177  33707  bnj1245  33715  bnj1311  33725  bnj1321  33728  bnj1388  33734  bnj1398  33735  bnj1415  33739  bnj1417  33742  bnj1421  33743  bnj1442  33750  bnj1452  33753  bnj1489  33757  bnj1312  33759  pthacycspth  33838  pconntop  33906  sconnpconn  33908  cvmcn  33943  cvmliftlem10  33975  sate0fv0  34098  fundmpss  34427  txpss3v  34539  pprodss4v  34545  outsideofcol  34794  fnebas  34892  filnetlem3  34928  bj-nnfe  35272  bj-xpcossxp  35733  bj-rvecmod  35839  pibt2  35961  phpreu  36135  matunitlindflem1  36147  matunitlindflem2  36148  matunitlindf  36149  poimirlem26  36177  itg2addnc  36205  istotbnd3  36303  totbndmet  36304  sstotbnd2  36306  sstotbnd  36307  equivtotbnd  36310  bndmet  36313  totbndbnd  36321  prdstotbnd  36326  smgrpismgmOLD  36394  mndoissmgrpOLD  36400  crngorngo  36532  prrngorngo  36583  divrngpr  36585  xrnss3v  36907  dfxrn2  36911  refressn  36978  antisymressn  36979  symrelim  37094  eqvrelsym  37140  eqvreltr  37142  disjorimxrn  37283  disjim  37316  disjlem14  37333  ollat  37748  omlol  37775  cvlatl  37860  hlomcmcv  37891  2dim  38006  1dimN  38007  lcfl8b  40040  lclkrlem2  40068  lclkrslem1  40073  lclkrslem2  40074  lcfrlem9  40086  mapdval2N  40166  mapdordlem2  40173  mapdrvallem2  40181  flddrngd  40780  nacsacs  41090  eldiophelnn0  41145  lnmlmod  41464  lnrring  41497  mncply  41522  idomrootle  41580  idomodle  41581  areaquad  41608  dfno2  41822  harval3  41932  alephiso3  41953  mnurndlem1  42683  nznngen  42718  binomcxplemcvg  42756  2uasbanh  42965  fompt  43533  disjinfi  43534  climxrre  44111  mbfdmssre  44361  stoweidlem14  44375  stoweidlem16  44377  stoweidlem24  44385  stoweidlem51  44412  stoweidlem54  44415  etransclem32  44627  sge0fodjrnlem  44777  pimrecltpos  45069  pimrecltneg  45085  smfaddlem1  45124  smflimsuplem7  45187  upwordisword  45240  ndmafv  45492  dfafv23  45605  dfatcolem  45607  dfatco  45608  evenz  45942  oddz  45943  gbeeven  46066  gbowodd  46067  rnghmsubcsetclem1  46393  funcrngcsetcALT  46417  rhmsubcsetclem1  46439  rhmsubcrngclem1  46445  ssnn0ssfz  46545  elbigof  46760  digvalnn0  46805  2sphere  46955  mof0  47024  mof0ALT  47026  thincc  47164