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  3347  rabidim1  3412  pssss  4039  eldifi  4072  elinel1  4142  ssunsn2  4771  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  7271  eqopi  7971  1st2nd2  7974  reldmtpos  8177  brinxper  8666  swoer  8668  ecopover  8761  sdomdom  8920  mapfien  9314  inf3lemd  9539  cardprclem  9894  infxpenlem  9926  cardinfima  10010  dfac5lem4  10039  dfac5lem4OLD  10041  domtriomlem  10355  smobeth  10500  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  axrnegex  11076  axpre-sup  11083  zre  12519  ixxss1  13307  ixxss2  13308  ixxss12  13309  lbioo  13320  ubioo  13321  iccss2  13361  rge0ssre  13400  elfzuz  13465  0wrd0  14493  01sqrexlem6  15200  rlimf  15454  lo1f  15471  lo1dm  15472  o1f  15482  o1dm  15483  mertenslem2  15841  divalglem9  16361  bitsinv2  16403  bitsf1ocnv  16404  gcdcllem1  16459  coprmproddvdslem  16622  prmnn  16634  prmuz2  16656  phimullem  16740  hashgcdlem  16749  1arith  16889  ramtlecl  16962  0ramcl  16985  firest  17386  acsmre  17609  posprs  18273  tospos  18375  latpos  18395  clatpos  18458  dlatl  18481  pslem  18529  tsrlemax  18543  tsrps  18544  chnwrd  18565  sgrpmgm  18683  mndsgrp  18699  grpmnd  18907  nsgsubg  19124  ghmgrp1  19184  ghmgrp2  19185  gimghm  19230  gagrp  19258  gaset  19259  psgneu  19472  efgredeu  19718  ablgrp  19751  cmnmnd  19763  cyggenod2  19851  cyggrp  19856  dprd2dlem1  20009  dprd2da  20010  ablfac2  20057  simpggrp  20062  ogrpgrp  20091  crngring  20217  dvdsrcl  20336  unitcl  20346  rimrhm  20464  brric2  20474  nzrringOLD  20485  subrgring  20542  subrgrcl  20544  rnghmsubcsetclem1  20599  funcrngcsetcALT  20609  rhmsubcsetclem1  20628  rhmsubcrngclem1  20634  domnnzr  20674  drngring  20704  flddrngd  20709  rng1nfld  20747  srngrhm  20813  ofldfld  20840  ofldlt1  20843  lmimlmhm  21051  lveclmod  21093  2idlelbas  21254  rng2idlsubgsubrng  21258  2idlcpblrng  21261  2idlcpbl  21262  qus1  21264  qusrhm  21266  lpirring  21321  cygznlem1  21556  cygznlem3  21559  ofldchr  21566  lbslinds  21823  assalmod  21850  assaring  21851  gsummatr01lem1  22630  topontop  22888  tpstop  22912  mretopd  23067  neiptoptop  23106  perftop  23131  restfpw  23154  cntop1  23215  cntop2  23216  cnptop1  23217  cnptop2  23218  cnprcl  23220  t1ficld  23302  t0top  23304  t1top  23305  haustop  23306  regtop  23308  nrmtop  23311  cnrmtop  23312  pnrmnrm  23315  cmptop  23370  tgcmp  23376  conndisj  23391  conntop  23392  1stctop  23418  llytop  23447  nllytop  23448  hmeocn  23735  filfbas  23823  ufilfil  23879  flimtop  23940  flimfil  23944  alexsublem  24019  ptcmplem3  24029  tsmsfbas  24103  tsmslem1  24104  tsmsgsum  24114  tsmssubm  24118  tsmsres  24119  tsmsf1o  24120  tsmsmhm  24121  tsmsadd  24122  tsmsxplem1  24128  tsmsxplem2  24129  tsmsxp  24130  tlmtmd  24162  tlmlmod  24164  tlmtrg  24165  tvctlm  24172  ressust  24238  uspreg  24248  ucncn  24259  neipcfilu  24270  cuspusp  24274  metxmet  24309  xmstps  24428  msxms  24429  xmsxmet  24431  msmet  24432  nrgngp  24637  nlmngp  24652  nlmlmod  24653  nlmnrg  24654  nvcnlm  24671  nmoi  24703  nghmrcl1  24707  nghmrcl2  24708  nmhmrcl1  24722  nmhmrcl2  24723  qdensere  24744  xrge0gsumle  24809  xrge0tsms  24810  icopnfcnv  24919  cvsclm  25103  cphsscph  25228  cmetmet  25263  cmsms  25325  hlbn  25340  ovolicc2lem5  25498  mblss  25508  mbff  25602  mbfres  25621  i1fmbf  25652  limcmpt  25860  c1liplem1  25973  c1lip2  25975  fta1glem1  26143  fta1glem2  26144  fta1g  26145  fta1b  26147  idomrootle  26148  ply1pid  26158  aacn  26294  ulmf2  26362  logdmnrp  26618  logdmss  26619  logcnlem2  26620  logcnlem3  26621  logcnlem4  26622  logcnlem5  26623  logcn  26624  dvloglem  26625  logf1o2  26627  efopnlem1  26633  logtayl2  26639  cxpcn  26722  cxpcn3lem  26724  cxpcn3  26725  resqrtcn  26726  atandmneg  26883  atandmcj  26886  cosatan  26898  cosatanne0  26899  birthdaylem1  26928  areacl  26939  cxp2lim  26954  jensenlem2  26965  jensen  26966  sqff1o  27159  mpodvdsmulf1o  27171  dvdsmulf1o  27173  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  lgseisenlem3  27354  chebbnd1  27449  chtppilim  27452  chpchtlim  27456  chpo1ub  27457  dchrmusumlema  27470  dchrvmasumiflem1  27478  dchrisum0lema  27491  dchrisum0lem2  27495  selberg3lem2  27535  pntrsumo1  27542  selbergsb  27552  pnt2  27590  ltsres  27640  noseponlem  27642  reno  28498  tglineeltr  28713  axcontlem2  29048  axcontlem7  29053  axcontlem8  29054  uhgr0vb  29155  lfuhgr1v0e  29337  fusgrusgr  29405  uvtxisvtx  29472  nbupgruvtxres  29490  cusgrusgr  29502  trliswlk  29779  clwlkiswlk  29857  clwwlkclwwlkn  30115  eupthistrl  30296  frgrusgr  30346  frgrwopreglem5  30406  clwwnonrepclwwnon  30430  ablogrpo  30633  bnnv  30952  hlobn  30974  hcauseq  31271  hlimseqi  31275  hlimveci  31276  shss  31296  sh0  31302  chsh  31310  lnopf  31945  bdopln  31947  hmopf  31960  lnfnf  31970  unopf1o  32002  elunop2  32099  elpjhmop  32271  stcltrlem1  32362  mdslle1i  32403  mdslle2i  32404  2reu2rex1  32565  2reureurex  32566  ssnnssfz  32875  xrge0tsmsd  33149  isarchiofld  33275  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  isdrng4  33371  reofld  33418  rearchi  33421  quslsm  33480  ufdidom  33617  mplvrpmga  33704  srafldlvec  33745  rgmoddimOLD  33770  extdggt0  33817  fldextid  33819  extdgid  33820  extdgmul  33823  extdg1id  33826  ist0cld  33993  creftop  34006  lmxrge0  34112  qqhrhm  34149  esumpcvgval  34238  dynkin  34327  measssd  34375  elmbfmvol2  34427  omssubadd  34460  sibfinima  34499  eulerpartlemr  34534  eulerpartlemgf  34539  fiblem  34558  domprobmeas  34570  ballotlemscr  34679  ballotlemfg  34686  ballotlemfrc  34687  ballotlemfrceq  34689  ballotlemrinv0  34693  chtvalz  34789  bnj563  34902  bnj658  34910  bnj667  34911  bnj570  35063  bnj938  35095  bnj1001  35117  bnj1006  35118  bnj1049  35132  bnj1121  35143  bnj1173  35160  bnj1177  35164  bnj1245  35172  bnj1311  35182  bnj1321  35185  bnj1388  35191  bnj1398  35192  bnj1415  35196  bnj1417  35199  bnj1421  35200  bnj1442  35207  bnj1452  35210  bnj1489  35214  bnj1312  35216  pthacycspth  35355  pconntop  35423  sconnpconn  35425  cvmcn  35460  cvmliftlem10  35492  sate0fv0  35615  fundmpss  35965  txpss3v  36074  pprodss4v  36080  outsideofcol  36331  fnebas  36542  filnetlem3  36578  bj-nnfe  37044  bj-xpcossxp  37519  bj-rvecmod  37625  pibt2  37747  phpreu  37939  matunitlindflem1  37951  matunitlindflem2  37952  matunitlindf  37953  poimirlem26  37981  itg2addnc  38009  istotbnd3  38106  totbndmet  38107  sstotbnd2  38109  sstotbnd  38110  equivtotbnd  38113  bndmet  38116  totbndbnd  38124  prdstotbnd  38129  smgrpismgmOLD  38197  mndoissmgrpOLD  38203  crngorngo  38335  prrngorngo  38386  divrngpr  38388  xrnss3v  38716  dfxrn2  38720  refressn  38868  antisymressn  38869  symrelim  38978  eqvrelsym  39024  eqvreltr  39026  disjimeceqim  39139  disjorimxrn  39183  disjim  39219  disjlem14  39236  ollat  39673  omlol  39700  cvlatl  39785  hlomcmcv  39816  2dim  39930  1dimN  39931  lcfl8b  41964  lclkrlem2  41992  lclkrslem1  41997  lclkrslem2  41998  lcfrlem9  42010  mapdval2N  42090  mapdordlem2  42097  mapdrvallem2  42105  idomnnzgmulnz  42586  aks6d1c6lem3  42625  readvrec2  42807  readvrec  42808  readvcot  42810  nacsacs  43155  eldiophelnn0  43210  lnmlmod  43525  lnrring  43558  mncply  43583  idomodle  43637  areaquad  43662  dfno2  43873  harval3  43983  alephiso3  44004  mnurndlem1  44726  nznngen  44761  binomcxplemcvg  44799  2uasbanh  45006  relpf  45395  disjinfi  45640  climxrre  46196  mbfdmssre  46446  stoweidlem14  46460  stoweidlem16  46462  stoweidlem24  46470  stoweidlem51  46497  stoweidlem54  46500  etransclem32  46712  sge0fodjrnlem  46862  pimrecltpos  47154  pimrecltneg  47170  smfaddlem1  47209  smflimsuplem7  47272  ndmafv  47600  dfafv23  47713  dfatcolem  47715  dfatco  47716  evenz  48118  oddz  48119  gbeeven  48242  gbowodd  48243  sclnbgrisvtx  48337  grlimgredgex  48488  ssnn0ssfz  48837  elbigof  49042  digvalnn0  49087  2sphere  49237  mof0  49325  mof0ALT  49327  uobeq2  49888  thincc  49909  termcthin  49964