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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  an3  655  xoror  1503  sbequ2OLD  2470  sbequ2ALT  2536  euex  2624  rabidim1  3341  reurex  3393  eqimss  3950  pssss  3999  eldifi  4030  elinel1  4099  ssunsn2  4673  pwssun  5351  sopo  5387  wefr  5440  opelxp1  5491  relop  5614  ssrelrn  5656  ordtr  6087  funmo  6248  funrel  6249  fnfun  6330  ffn  6389  f1f  6450  f1of1  6489  f1ofo  6497  isof1o  6946  eqopi  7588  1st2nd2  7591  reldmtpos  7758  swoer  8176  ecopover  8258  sdomdom  8392  mapfien  8724  inf3lemd  8943  cardprclem  9261  infxpenlem  9292  cardinfima  9376  dfac5lem4  9405  domtriomlem  9717  smobeth  9861  fpwwe2lem6  9910  fpwwe2lem7  9911  fpwwe2lem12  9916  fpwwe2lem13  9917  fpwwe2  9918  axrnegex  10437  axpre-sup  10444  zre  11839  ixxss1  12610  ixxss2  12611  ixxss12  12612  lbioo  12623  ubioo  12624  iccss2  12661  rge0ssre  12698  elfzuz  12758  0wrd0  13740  splfv1  13957  sqrlem6  14445  rlimf  14696  lo1f  14713  lo1dm  14714  o1f  14724  o1dm  14725  mertenslem2  15078  divalglem9  15589  bitsinv2  15629  bitsf1ocnv  15630  gcdcllem1  15685  coprmproddvdslem  15839  prmnn  15851  prmuz2  15873  phimullem  15949  hashgcdlem  15958  1arith  16096  ramtlecl  16169  0ramcl  16192  firest  16539  acsmre  16756  posprs  17392  latpos  17493  clatpos  17553  dlatl  17638  pslem  17649  tsrlemax  17663  tsrps  17664  sgrpmgm  17732  mndsgrp  17742  grpmnd  17872  nsgsubg  18069  ghmgrp1  18105  ghmgrp2  18106  gimghm  18149  gagrp  18167  gaset  18168  psgneu  18369  efgredeu  18609  ablgrp  18642  cmnmnd  18652  cyggenod2  18731  cyggrp  18735  dprd2dlem1  18884  dprd2da  18885  ablfac2  18932  crngring  19002  dvdsrcl  19093  unitcl  19103  brric2  19194  drngring  19203  subrgring  19232  subrgrcl  19234  srngrhm  19316  lmimlmhm  19530  lveclmod  19572  2idlcpbl  19700  qus1  19701  qusrhm  19703  lpirring  19718  nzrring  19727  domnnzr  19761  fldidom  19771  assalmod  19785  assaring  19786  assasca  19787  cygznlem1  20399  cygznlem3  20402  lbslinds  20663  gsummatr01lem1  20952  topontop  21209  tpstop  21233  mretopd  21388  neiptoptop  21427  perftop  21452  restfpw  21475  cntop1  21536  cntop2  21537  cnptop1  21538  cnptop2  21539  cnprcl  21541  t1ficld  21623  t0top  21625  t1top  21626  haustop  21627  regtop  21629  nrmtop  21632  cnrmtop  21633  pnrmnrm  21636  cmptop  21691  tgcmp  21697  conndisj  21712  conntop  21713  1stctop  21739  llytop  21768  nllytop  21769  hmeocn  22056  filfbas  22144  ufilfil  22200  flimtop  22261  flimfil  22265  alexsublem  22340  ptcmplem3  22350  tsmsfbas  22423  tsmslem1  22424  tsmsgsum  22434  tsmssubm  22438  tsmsres  22439  tsmsf1o  22440  tsmsmhm  22441  tsmsadd  22442  tsmsxplem1  22448  tsmsxplem2  22449  tsmsxp  22450  tlmtmd  22482  tlmlmod  22484  tlmtrg  22485  tvctlm  22492  ressust  22560  uspreg  22570  ucncn  22581  neipcfilu  22592  cuspusp  22596  metxmet  22631  xmstps  22750  msxms  22751  xmsxmet  22753  msmet  22754  nrgngp  22958  nlmngp  22973  nlmlmod  22974  nlmnrg  22975  nvcnlm  22992  nmoi  23024  nghmrcl1  23028  nghmrcl2  23029  nmhmrcl1  23043  nmhmrcl2  23044  qdensere  23065  xrge0gsumle  23128  xrge0tsms  23129  icopnfcnv  23233  cvsclm  23417  cphsscph  23541  cmetmet  23576  cmsms  23638  hlbn  23653  ovolicc2lem5  23809  mblss  23819  mbff  23913  mbfres  23932  i1fmbf  23963  limcmpt  24168  c1liplem1  24280  c1lip2  24282  fta1glem1  24446  fta1glem2  24447  fta1g  24448  fta1b  24450  ply1pid  24460  aacn  24593  ulmf2  24659  logdmnrp  24909  logdmss  24910  logcnlem2  24911  logcnlem3  24912  logcnlem4  24913  logcnlem5  24914  logcn  24915  dvloglem  24916  logf1o2  24918  efopnlem1  24924  logtayl2  24930  cxpcn  25011  cxpcn3lem  25013  cxpcn3  25014  resqrtcn  25015  atandmneg  25169  atandmcj  25172  cosatan  25184  cosatanne0  25185  birthdaylem1  25215  areacl  25226  cxp2lim  25240  jensenlem2  25251  jensen  25252  sqff1o  25445  dvdsmulf1o  25457  lgsqrlem1  25608  lgsqrlem2  25609  lgsqrlem3  25610  lgsqrlem4  25611  lgseisenlem3  25639  chebbnd1  25734  chtppilim  25737  chpchtlim  25741  chpo1ub  25742  dchrmusumlema  25755  dchrvmasumiflem1  25763  dchrisum0lema  25776  dchrisum0lem2  25780  selberg3lem2  25820  pntrsumo1  25827  selbergsb  25837  pnt2  25875  tglineeltr  26103  axcontlem2  26438  axcontlem7  26443  axcontlem8  26444  uhgr0vb  26544  lfuhgr1v0e  26723  fusgrusgr  26791  uvtxisvtx  26858  nbupgruvtxres  26876  cusgrusgr  26888  trliswlk  27165  clwlkiswlk  27241  clwwlkclwwlkn  27494  eupthistrl  27676  frgrusgr  27727  frgrwopreglem5  27788  clwwnonrepclwwnon  27812  ablogrpo  28011  bnnv  28330  hlobn  28352  hcauseq  28649  hlimseqi  28653  hlimveci  28654  shss  28674  sh0  28680  chsh  28688  lnopf  29323  bdopln  29325  hmopf  29338  lnfnf  29348  unopf1o  29380  elunop2  29477  elpjhmop  29649  stcltrlem1  29740  mdslle1i  29781  mdslle2i  29782  2reu2rex1  29932  2reureurex  29933  ssnnssfz  30194  tospos  30315  ogrpgrp  30360  xrge0tsmsd  30499  ofldfld  30533  ofldlt1  30536  ofldchr  30537  isarchiofld  30540  reofld  30563  rearchi  30565  srafldlvec  30591  rgmoddim  30608  extdggt0  30647  fldextid  30649  extdgmul  30651  extdg1id  30653  creftop  30723  lmxrge0  30808  qqhrhm  30843  esumpcvgval  30950  dynkin  31039  measssd  31087  elmbfmvol2  31138  omssubadd  31171  sibfinima  31210  eulerpartlemr  31245  eulerpartlemgf  31250  fiblem  31269  domprobmeas  31281  ballotlemscr  31389  ballotlemfg  31396  ballotlemfrc  31397  ballotlemfrceq  31399  ballotlemrinv0  31403  chtvalz  31513  bnj563  31627  bnj658  31635  bnj667  31636  bnj570  31789  bnj938  31821  bnj1001  31842  bnj1006  31843  bnj1049  31856  bnj1121  31867  bnj1173  31884  bnj1177  31888  bnj1245  31896  bnj1311  31906  bnj1321  31909  bnj1388  31915  bnj1398  31916  bnj1415  31920  bnj1417  31923  bnj1421  31924  bnj1442  31931  bnj1452  31934  bnj1489  31938  bnj1312  31940  pthacycspth  32014  pconntop  32082  sconnpconn  32084  cvmcn  32119  cvmliftlem10  32151  sate0fv0  32274  fundmpss  32619  sltres  32780  noseponlem  32782  txpss3v  32950  pprodss4v  32956  outsideofcol  33205  fnebas  33303  filnetlem3  33339  bj-nnfe  33859  bj-epelg  33980  pibt2  34250  phpreu  34428  matunitlindflem1  34440  matunitlindflem2  34441  matunitlindf  34442  poimirlem26  34470  itg2addnc  34498  istotbnd3  34602  totbndmet  34603  sstotbnd2  34605  sstotbnd  34606  equivtotbnd  34609  bndmet  34612  totbndbnd  34620  prdstotbnd  34625  smgrpismgmOLD  34693  mndoissmgrpOLD  34699  crngorngo  34831  prrngorngo  34882  divrngpr  34884  xrnss3v  35176  dfxrn2  35180  symrelim  35347  eqvrelsym  35392  eqvreltr  35394  disjorimxrn  35530  ollat  35901  omlol  35928  cvlatl  36013  hlomcmcv  36044  2dim  36158  1dimN  36159  lcfl8b  38192  lclkrlem2  38220  lclkrslem1  38225  lclkrslem2  38226  lcfrlem9  38238  mapdval2N  38318  mapdordlem2  38325  mapdrvallem2  38333  nacsacs  38812  eldiophelnn0  38867  lnmlmod  39185  lnrring  39218  mncply  39243  idomrootle  39301  idomodle  39302  areaquad  39329  harval3  39410  alephiso3  39424  mnurndlem1  40135  simpggrp  40171  nznngen  40207  binomcxplemcvg  40245  2uasbanh  40455  fompt  41014  disjinfi  41015  climxrre  41594  mbfdmssre  41849  stoweidlem14  41863  stoweidlem16  41865  stoweidlem24  41873  stoweidlem51  41900  stoweidlem54  41903  etransclem32  42115  sge0fodjrnlem  42262  pimrecltpos  42551  pimrecltneg  42565  smfaddlem1  42603  smflimsuplem7  42664  ndmafv  42877  dfafv23  42990  dfatcolem  42992  dfatco  42993  evenz  43299  oddz  43300  gbeeven  43423  gbowodd  43424  rnghmsubcsetclem1  43746  funcrngcsetcALT  43770  rhmsubcsetclem1  43792  rhmsubcrngclem1  43798  ssnn0ssfz  43897  elbigof  44117  digvalnn0  44162  2sphere  44239