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  2572  reurex  3350  rabidim1  3417  pssss  4048  eldifi  4081  elinel1  4151  ssunsn2  4779  pwssun  5508  sopo  5543  wefr  5606  opelxp1  5658  relop  5790  ssrelrn  5834  ordtr  6320  funmo  6497  funrel  6498  fnfun  6581  ffn  6651  f1f  6719  f1of1  6762  f1ofo  6770  isof1o  7257  eqopi  7957  1st2nd2  7960  reldmtpos  8164  brinxper  8651  swoer  8653  ecopover  8745  sdomdom  8902  mapfien  9292  inf3lemd  9517  cardprclem  9869  infxpenlem  9901  cardinfima  9985  dfac5lem4  10014  dfac5lem4OLD  10016  domtriomlem  10330  smobeth  10474  fpwwe2lem5  10523  fpwwe2lem6  10524  fpwwe2lem11  10529  fpwwe2lem12  10530  fpwwe2  10531  axrnegex  11050  axpre-sup  11057  zre  12469  ixxss1  13260  ixxss2  13261  ixxss12  13262  lbioo  13273  ubioo  13274  iccss2  13314  rge0ssre  13353  elfzuz  13417  0wrd0  14444  01sqrexlem6  15151  rlimf  15405  lo1f  15422  lo1dm  15423  o1f  15433  o1dm  15434  mertenslem2  15789  divalglem9  16309  bitsinv2  16351  bitsf1ocnv  16352  gcdcllem1  16407  coprmproddvdslem  16570  prmnn  16582  prmuz2  16604  phimullem  16687  hashgcdlem  16696  1arith  16836  ramtlecl  16909  0ramcl  16932  firest  17333  acsmre  17555  posprs  18219  tospos  18321  latpos  18341  clatpos  18404  dlatl  18427  pslem  18475  tsrlemax  18489  tsrps  18490  chnwrd  18511  sgrpmgm  18629  mndsgrp  18645  grpmnd  18850  nsgsubg  19068  ghmgrp1  19128  ghmgrp2  19129  gimghm  19174  gagrp  19202  gaset  19203  psgneu  19416  efgredeu  19662  ablgrp  19695  cmnmnd  19707  cyggenod2  19795  cyggrp  19800  dprd2dlem1  19953  dprd2da  19954  ablfac2  20001  simpggrp  20006  ogrpgrp  20035  crngring  20161  dvdsrcl  20281  unitcl  20291  rimrhm  20409  brric2  20419  nzrringOLD  20430  subrgring  20487  subrgrcl  20489  rnghmsubcsetclem1  20544  funcrngcsetcALT  20554  rhmsubcsetclem1  20573  rhmsubcrngclem1  20579  domnnzr  20619  drngring  20649  flddrngd  20654  rng1nfld  20692  srngrhm  20758  ofldfld  20785  ofldlt1  20788  lmimlmhm  20996  lveclmod  21038  2idlelbas  21199  rng2idlsubgsubrng  21203  2idlcpblrng  21206  2idlcpbl  21207  qus1  21209  qusrhm  21211  lpirring  21266  cygznlem1  21501  cygznlem3  21504  ofldchr  21511  lbslinds  21768  assalmod  21795  assaring  21796  gsummatr01lem1  22568  topontop  22826  tpstop  22850  mretopd  23005  neiptoptop  23044  perftop  23069  restfpw  23092  cntop1  23153  cntop2  23154  cnptop1  23155  cnptop2  23156  cnprcl  23158  t1ficld  23240  t0top  23242  t1top  23243  haustop  23244  regtop  23246  nrmtop  23249  cnrmtop  23250  pnrmnrm  23253  cmptop  23308  tgcmp  23314  conndisj  23329  conntop  23330  1stctop  23356  llytop  23385  nllytop  23386  hmeocn  23673  filfbas  23761  ufilfil  23817  flimtop  23878  flimfil  23882  alexsublem  23957  ptcmplem3  23967  tsmsfbas  24041  tsmslem1  24042  tsmsgsum  24052  tsmssubm  24056  tsmsres  24057  tsmsf1o  24058  tsmsmhm  24059  tsmsadd  24060  tsmsxplem1  24066  tsmsxplem2  24067  tsmsxp  24068  tlmtmd  24100  tlmlmod  24102  tlmtrg  24103  tvctlm  24110  ressust  24176  uspreg  24186  ucncn  24197  neipcfilu  24208  cuspusp  24212  metxmet  24247  xmstps  24366  msxms  24367  xmsxmet  24369  msmet  24370  nrgngp  24575  nlmngp  24590  nlmlmod  24591  nlmnrg  24592  nvcnlm  24609  nmoi  24641  nghmrcl1  24645  nghmrcl2  24646  nmhmrcl1  24660  nmhmrcl2  24661  qdensere  24682  xrge0gsumle  24747  xrge0tsms  24748  icopnfcnv  24865  cvsclm  25051  cphsscph  25176  cmetmet  25211  cmsms  25273  hlbn  25288  ovolicc2lem5  25447  mblss  25457  mbff  25551  mbfres  25570  i1fmbf  25601  limcmpt  25809  c1liplem1  25926  c1lip2  25928  fta1glem1  26098  fta1glem2  26099  fta1g  26100  fta1b  26102  idomrootle  26103  ply1pid  26113  aacn  26250  ulmf2  26318  logdmnrp  26575  logdmss  26576  logcnlem2  26577  logcnlem3  26578  logcnlem4  26579  logcnlem5  26580  logcn  26581  dvloglem  26582  logf1o2  26584  efopnlem1  26590  logtayl2  26596  cxpcn  26679  cxpcnOLD  26680  cxpcn3lem  26682  cxpcn3  26683  resqrtcn  26684  atandmneg  26841  atandmcj  26844  cosatan  26856  cosatanne0  26857  birthdaylem1  26886  areacl  26897  cxp2lim  26912  jensenlem2  26923  jensen  26924  sqff1o  27117  mpodvdsmulf1o  27129  dvdsmulf1o  27131  lgsqrlem1  27282  lgsqrlem2  27283  lgsqrlem3  27284  lgsqrlem4  27285  lgseisenlem3  27313  chebbnd1  27408  chtppilim  27411  chpchtlim  27415  chpo1ub  27416  dchrmusumlema  27429  dchrvmasumiflem1  27437  dchrisum0lema  27450  dchrisum0lem2  27454  selberg3lem2  27494  pntrsumo1  27501  selbergsb  27511  pnt2  27549  sltres  27599  noseponlem  27601  tglineeltr  28607  axcontlem2  28941  axcontlem7  28946  axcontlem8  28947  uhgr0vb  29048  lfuhgr1v0e  29230  fusgrusgr  29298  uvtxisvtx  29365  nbupgruvtxres  29383  cusgrusgr  29395  trliswlk  29672  clwlkiswlk  29750  clwwlkclwwlkn  30005  eupthistrl  30186  frgrusgr  30236  frgrwopreglem5  30296  clwwnonrepclwwnon  30320  ablogrpo  30522  bnnv  30841  hlobn  30863  hcauseq  31160  hlimseqi  31164  hlimveci  31165  shss  31185  sh0  31191  chsh  31199  lnopf  31834  bdopln  31836  hmopf  31849  lnfnf  31859  unopf1o  31891  elunop2  31988  elpjhmop  32160  stcltrlem1  32251  mdslle1i  32292  mdslle2i  32293  2reu2rex1  32455  2reureurex  32456  ssnnssfz  32765  xrge0tsmsd  33037  isarchiofld  33163  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem4  33207  isdrng4  33256  reofld  33303  rearchi  33306  quslsm  33365  ufdidom  33502  mplvrpmga  33570  srafldlvec  33593  rgmoddimOLD  33618  extdggt0  33665  fldextid  33667  extdgid  33668  extdgmul  33671  extdg1id  33674  ist0cld  33841  creftop  33854  lmxrge0  33960  qqhrhm  33997  esumpcvgval  34086  dynkin  34175  measssd  34223  elmbfmvol2  34275  omssubadd  34308  sibfinima  34347  eulerpartlemr  34382  eulerpartlemgf  34387  fiblem  34406  domprobmeas  34418  ballotlemscr  34527  ballotlemfg  34534  ballotlemfrc  34535  ballotlemfrceq  34537  ballotlemrinv0  34541  chtvalz  34637  bnj563  34750  bnj658  34758  bnj667  34759  bnj570  34912  bnj938  34944  bnj1001  34966  bnj1006  34967  bnj1049  34981  bnj1121  34992  bnj1173  35009  bnj1177  35013  bnj1245  35021  bnj1311  35031  bnj1321  35034  bnj1388  35040  bnj1398  35041  bnj1415  35045  bnj1417  35048  bnj1421  35049  bnj1442  35056  bnj1452  35059  bnj1489  35063  bnj1312  35065  pthacycspth  35189  pconntop  35257  sconnpconn  35259  cvmcn  35294  cvmliftlem10  35326  sate0fv0  35449  fundmpss  35799  txpss3v  35911  pprodss4v  35917  outsideofcol  36166  fnebas  36377  filnetlem3  36413  bj-nnfe  36764  bj-xpcossxp  37222  bj-rvecmod  37328  pibt2  37450  phpreu  37643  matunitlindflem1  37655  matunitlindflem2  37656  matunitlindf  37657  poimirlem26  37685  itg2addnc  37713  istotbnd3  37810  totbndmet  37811  sstotbnd2  37813  sstotbnd  37814  equivtotbnd  37817  bndmet  37820  totbndbnd  37828  prdstotbnd  37833  smgrpismgmOLD  37901  mndoissmgrpOLD  37907  crngorngo  38039  prrngorngo  38090  divrngpr  38092  xrnss3v  38399  dfxrn2  38403  refressn  38479  antisymressn  38480  symrelim  38595  eqvrelsym  38641  eqvreltr  38643  disjorimxrn  38785  disjim  38818  disjlem14  38835  ollat  39251  omlol  39278  cvlatl  39363  hlomcmcv  39394  2dim  39508  1dimN  39509  lcfl8b  41542  lclkrlem2  41570  lclkrslem1  41575  lclkrslem2  41576  lcfrlem9  41588  mapdval2N  41668  mapdordlem2  41675  mapdrvallem2  41683  idomnnzgmulnz  42165  aks6d1c6lem3  42204  readvrec2  42393  readvrec  42394  readvcot  42396  nacsacs  42741  eldiophelnn0  42796  lnmlmod  43111  lnrring  43144  mncply  43169  idomodle  43223  areaquad  43248  dfno2  43460  harval3  43570  alephiso3  43591  mnurndlem1  44313  nznngen  44348  binomcxplemcvg  44386  2uasbanh  44593  relpf  44982  disjinfi  45228  climxrre  45787  mbfdmssre  46037  stoweidlem14  46051  stoweidlem16  46053  stoweidlem24  46061  stoweidlem51  46088  stoweidlem54  46091  etransclem32  46303  sge0fodjrnlem  46453  pimrecltpos  46745  pimrecltneg  46761  smfaddlem1  46800  smflimsuplem7  46863  ndmafv  47170  dfafv23  47283  dfatcolem  47285  dfatco  47286  evenz  47660  oddz  47661  gbeeven  47784  gbowodd  47785  sclnbgrisvtx  47879  grlimgredgex  48030  ssnn0ssfz  48379  elbigof  48585  digvalnn0  48630  2sphere  48780  mof0  48868  mof0ALT  48870  uobeq2  49432  thincc  49453  termcthin  49508