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  2570  reurex  3349  rabidim1  3419  pssss  4051  eldifi  4084  elinel1  4154  ssunsn2  4781  pwssun  5515  sopo  5550  wefr  5613  opelxp1  5665  relop  5797  ssrelrn  5841  ordtr  6325  funmo  6502  funrel  6503  fnfun  6586  ffn  6656  f1f  6724  f1of1  6767  f1ofo  6775  isof1o  7264  eqopi  7967  1st2nd2  7970  reldmtpos  8174  brinxper  8661  swoer  8663  ecopover  8755  sdomdom  8912  mapfien  9317  inf3lemd  9542  cardprclem  9894  infxpenlem  9926  cardinfima  10010  dfac5lem4  10039  dfac5lem4OLD  10041  domtriomlem  10355  smobeth  10499  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  axrnegex  11075  axpre-sup  11082  zre  12493  ixxss1  13284  ixxss2  13285  ixxss12  13286  lbioo  13297  ubioo  13298  iccss2  13338  rge0ssre  13377  elfzuz  13441  0wrd0  14465  01sqrexlem6  15172  rlimf  15426  lo1f  15443  lo1dm  15444  o1f  15454  o1dm  15455  mertenslem2  15810  divalglem9  16330  bitsinv2  16372  bitsf1ocnv  16373  gcdcllem1  16428  coprmproddvdslem  16591  prmnn  16603  prmuz2  16625  phimullem  16708  hashgcdlem  16717  1arith  16857  ramtlecl  16930  0ramcl  16953  firest  17354  acsmre  17576  posprs  18240  tospos  18342  latpos  18362  clatpos  18425  dlatl  18448  pslem  18496  tsrlemax  18510  tsrps  18511  sgrpmgm  18616  mndsgrp  18632  grpmnd  18837  nsgsubg  19055  ghmgrp1  19115  ghmgrp2  19116  gimghm  19161  gagrp  19189  gaset  19190  psgneu  19403  efgredeu  19649  ablgrp  19682  cmnmnd  19694  cyggenod2  19782  cyggrp  19787  dprd2dlem1  19940  dprd2da  19941  ablfac2  19988  simpggrp  19993  ogrpgrp  20022  crngring  20148  dvdsrcl  20268  unitcl  20278  rimrhmOLD  20398  rimrhm  20399  brric2  20409  nzrringOLD  20420  subrgring  20477  subrgrcl  20479  rnghmsubcsetclem1  20534  funcrngcsetcALT  20544  rhmsubcsetclem1  20563  rhmsubcrngclem1  20569  domnnzr  20609  drngring  20639  flddrngd  20644  rng1nfld  20682  srngrhm  20748  ofldfld  20775  ofldlt1  20778  lmimlmhm  20986  lveclmod  21028  2idlelbas  21189  rng2idlsubgsubrng  21193  2idlcpblrng  21196  2idlcpbl  21197  qus1  21199  qusrhm  21201  lpirring  21256  cygznlem1  21491  cygznlem3  21494  ofldchr  21501  lbslinds  21758  assalmod  21785  assaring  21786  gsummatr01lem1  22558  topontop  22816  tpstop  22840  mretopd  22995  neiptoptop  23034  perftop  23059  restfpw  23082  cntop1  23143  cntop2  23144  cnptop1  23145  cnptop2  23146  cnprcl  23148  t1ficld  23230  t0top  23232  t1top  23233  haustop  23234  regtop  23236  nrmtop  23239  cnrmtop  23240  pnrmnrm  23243  cmptop  23298  tgcmp  23304  conndisj  23319  conntop  23320  1stctop  23346  llytop  23375  nllytop  23376  hmeocn  23663  filfbas  23751  ufilfil  23807  flimtop  23868  flimfil  23872  alexsublem  23947  ptcmplem3  23957  tsmsfbas  24031  tsmslem1  24032  tsmsgsum  24042  tsmssubm  24046  tsmsres  24047  tsmsf1o  24048  tsmsmhm  24049  tsmsadd  24050  tsmsxplem1  24056  tsmsxplem2  24057  tsmsxp  24058  tlmtmd  24090  tlmlmod  24092  tlmtrg  24093  tvctlm  24100  ressust  24167  uspreg  24177  ucncn  24188  neipcfilu  24199  cuspusp  24203  metxmet  24238  xmstps  24357  msxms  24358  xmsxmet  24360  msmet  24361  nrgngp  24566  nlmngp  24581  nlmlmod  24582  nlmnrg  24583  nvcnlm  24600  nmoi  24632  nghmrcl1  24636  nghmrcl2  24637  nmhmrcl1  24651  nmhmrcl2  24652  qdensere  24673  xrge0gsumle  24738  xrge0tsms  24739  icopnfcnv  24856  cvsclm  25042  cphsscph  25167  cmetmet  25202  cmsms  25264  hlbn  25279  ovolicc2lem5  25438  mblss  25448  mbff  25542  mbfres  25561  i1fmbf  25592  limcmpt  25800  c1liplem1  25917  c1lip2  25919  fta1glem1  26089  fta1glem2  26090  fta1g  26091  fta1b  26093  idomrootle  26094  ply1pid  26104  aacn  26241  ulmf2  26309  logdmnrp  26566  logdmss  26567  logcnlem2  26568  logcnlem3  26569  logcnlem4  26570  logcnlem5  26571  logcn  26572  dvloglem  26573  logf1o2  26575  efopnlem1  26581  logtayl2  26587  cxpcn  26670  cxpcnOLD  26671  cxpcn3lem  26673  cxpcn3  26674  resqrtcn  26675  atandmneg  26832  atandmcj  26835  cosatan  26847  cosatanne0  26848  birthdaylem1  26877  areacl  26888  cxp2lim  26903  jensenlem2  26914  jensen  26915  sqff1o  27108  mpodvdsmulf1o  27120  dvdsmulf1o  27122  lgsqrlem1  27273  lgsqrlem2  27274  lgsqrlem3  27275  lgsqrlem4  27276  lgseisenlem3  27304  chebbnd1  27399  chtppilim  27402  chpchtlim  27406  chpo1ub  27407  dchrmusumlema  27420  dchrvmasumiflem1  27428  dchrisum0lema  27441  dchrisum0lem2  27445  selberg3lem2  27485  pntrsumo1  27492  selbergsb  27502  pnt2  27540  sltres  27590  noseponlem  27592  tglineeltr  28594  axcontlem2  28928  axcontlem7  28933  axcontlem8  28934  uhgr0vb  29035  lfuhgr1v0e  29217  fusgrusgr  29285  uvtxisvtx  29352  nbupgruvtxres  29370  cusgrusgr  29382  trliswlk  29659  clwlkiswlk  29737  clwwlkclwwlkn  29992  eupthistrl  30173  frgrusgr  30223  frgrwopreglem5  30283  clwwnonrepclwwnon  30307  ablogrpo  30509  bnnv  30828  hlobn  30850  hcauseq  31147  hlimseqi  31151  hlimveci  31152  shss  31172  sh0  31178  chsh  31186  lnopf  31821  bdopln  31823  hmopf  31836  lnfnf  31846  unopf1o  31878  elunop2  31975  elpjhmop  32147  stcltrlem1  32238  mdslle1i  32279  mdslle2i  32280  2reu2rex1  32443  2reureurex  32444  ssnnssfz  32743  chnwrd  32962  xrge0tsmsd  33028  isarchiofld  33151  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem4  33195  isdrng4  33244  reofld  33291  rearchi  33293  quslsm  33352  ufdidom  33489  srafldlvec  33558  rgmoddimOLD  33582  extdggt0  33629  fldextid  33631  extdgid  33632  extdgmul  33635  extdg1id  33637  ist0cld  33799  creftop  33812  lmxrge0  33918  qqhrhm  33955  esumpcvgval  34044  dynkin  34133  measssd  34181  elmbfmvol2  34234  omssubadd  34267  sibfinima  34306  eulerpartlemr  34341  eulerpartlemgf  34346  fiblem  34365  domprobmeas  34377  ballotlemscr  34486  ballotlemfg  34493  ballotlemfrc  34494  ballotlemfrceq  34496  ballotlemrinv0  34500  chtvalz  34596  bnj563  34709  bnj658  34717  bnj667  34718  bnj570  34871  bnj938  34903  bnj1001  34925  bnj1006  34926  bnj1049  34940  bnj1121  34951  bnj1173  34968  bnj1177  34972  bnj1245  34980  bnj1311  34990  bnj1321  34993  bnj1388  34999  bnj1398  35000  bnj1415  35004  bnj1417  35007  bnj1421  35008  bnj1442  35015  bnj1452  35018  bnj1489  35022  bnj1312  35024  pthacycspth  35129  pconntop  35197  sconnpconn  35199  cvmcn  35234  cvmliftlem10  35266  sate0fv0  35389  fundmpss  35739  txpss3v  35851  pprodss4v  35857  outsideofcol  36106  fnebas  36317  filnetlem3  36353  bj-nnfe  36704  bj-xpcossxp  37162  bj-rvecmod  37268  pibt2  37390  phpreu  37583  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  poimirlem26  37625  itg2addnc  37653  istotbnd3  37750  totbndmet  37751  sstotbnd2  37753  sstotbnd  37754  equivtotbnd  37757  bndmet  37760  totbndbnd  37768  prdstotbnd  37773  smgrpismgmOLD  37841  mndoissmgrpOLD  37847  crngorngo  37979  prrngorngo  38030  divrngpr  38032  xrnss3v  38339  dfxrn2  38343  refressn  38419  antisymressn  38420  symrelim  38535  eqvrelsym  38581  eqvreltr  38583  disjorimxrn  38725  disjim  38758  disjlem14  38775  ollat  39191  omlol  39218  cvlatl  39303  hlomcmcv  39334  2dim  39449  1dimN  39450  lcfl8b  41483  lclkrlem2  41511  lclkrslem1  41516  lclkrslem2  41517  lcfrlem9  41529  mapdval2N  41609  mapdordlem2  41616  mapdrvallem2  41624  idomnnzgmulnz  42106  aks6d1c6lem3  42145  readvrec2  42334  readvrec  42335  readvcot  42337  nacsacs  42682  eldiophelnn0  42737  lnmlmod  43052  lnrring  43085  mncply  43110  idomodle  43164  areaquad  43189  dfno2  43401  harval3  43511  alephiso3  43532  mnurndlem1  44254  nznngen  44289  binomcxplemcvg  44327  2uasbanh  44535  relpf  44924  disjinfi  45170  climxrre  45732  mbfdmssre  45982  stoweidlem14  45996  stoweidlem16  45998  stoweidlem24  46006  stoweidlem51  46033  stoweidlem54  46036  etransclem32  46248  sge0fodjrnlem  46398  pimrecltpos  46690  pimrecltneg  46706  smfaddlem1  46745  smflimsuplem7  46808  upwordisword  46863  ndmafv  47125  dfafv23  47238  dfatcolem  47240  dfatco  47241  evenz  47615  oddz  47616  gbeeven  47739  gbowodd  47740  sclnbgrisvtx  47834  grlimgredgex  47985  ssnn0ssfz  48334  elbigof  48540  digvalnn0  48585  2sphere  48735  mof0  48823  mof0ALT  48825  uobeq2  49387  thincc  49408  termcthin  49463