Theorem simplbi 475

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  an3  864  3simpa  1051  xoror  1463  sbequ2  1869  reurex  3137  eqimss  3620  pssss  3664  eldifi  3694  elinel1  3761  ssunsn2  4299  pwssun  4944  sopo  4976  wefr  5028  opelxp1  5074  relop  5194  ssrelrn  5237  ordtr  5654  funmo  5820  funrel  5821  fnfun  5902  ffn  5958  f1f  6014  f1of1  6049  f1ofo  6057  isof1o  6473  eqopi  7093  1st2nd2  7096  reldmtpos  7247  swoer  7659  erdisj  7681  ecopover  7738  ecopoverOLD  7739  sdomdom  7869  mapfien  8196  inf3lemd  8407  cardprclem  8688  infxpenlem  8719  cardinfima  8803  dfac5lem4  8832  domtriomlem  9147  smobeth  9287  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  axrnegex  9862  axpre-sup  9869  zre  11258  nnssz  11274  ixxss1  12064  ixxss2  12065  ixxss12  12066  lbioo  12077  ubioo  12078  iccss2  12115  rge0ssre  12151  elfzuz  12209  uzdisj  12282  nn0disj  12324  0wrd0  13186  splfv1  13357  sqrlem6  13836  rlimf  14080  lo1f  14097  lo1dm  14098  o1f  14108  o1dm  14109  mertenslem2  14456  fprodge0  14563  divalglem9  14962  bitsinv2  15003  bitsf1ocnv  15004  gcdcllem1  15059  coprmproddvdslem  15214  prmnn  15226  prmuz2  15246  phimullem  15322  hashgcdlem  15331  1arith  15469  ramtlecl  15542  0ramcl  15565  firest  15916  acsmre  16136  posprs  16772  latpos  16873  clatpos  16933  dlatl  17018  pslem  17029  tsrlemax  17043  tsrps  17044  sgrpmgm  17112  mndsgrp  17122  grpmnd  17252  nsgsubg  17449  ghmgrp1  17485  ghmgrp2  17486  gimghm  17529  gagrp  17548  gaset  17549  psgneu  17749  efgredeu  17988  ablgrp  18021  cmnmnd  18031  cyggenod2  18110  cyggrp  18114  ablfac2  18311  crngring  18381  dvdsrcl  18472  unitcl  18482  brric2  18568  drngring  18577  subrgring  18606  subrgrcl  18608  srngrhm  18674  lmimlmhm  18885  lveclmod  18927  2idlcpbl  19055  qus1  19056  qusrhm  19058  lpirring  19073  nzrring  19082  domnnzr  19116  fldidom  19126  assalmod  19140  assaring  19141  assasca  19142  cygznlem1  19734  cygznlem3  19737  lbslinds  19991  gsummatr01lem1  20280  topontop  20541  tpstop  20554  clsval2  20664  mretopd  20706  neiptoptop  20745  perftop  20770  restfpw  20793  cntop1  20854  cntop2  20855  cnptop1  20856  cnptop2  20857  cnprcl  20859  t1ficld  20941  t0top  20943  t1top  20944  haustop  20945  regtop  20947  nrmtop  20950  cnrmtop  20951  pnrmnrm  20954  cmptop  21008  discmp  21011  tgcmp  21014  uncmp  21016  conndisj  21029  contop  21030  1stctop  21056  llytop  21085  nllytop  21086  hmeocn  21373  filfbas  21462  ufilfil  21518  flimtop  21579  flimfil  21583  alexsublem  21658  ptcmplem3  21668  tsmsfbas  21741  tsmslem1  21742  tsmsgsum  21752  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  tsmsmhm  21759  tsmsadd  21760  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  tlmtmd  21800  tlmlmod  21802  tlmtrg  21803  tvctlm  21810  ressust  21878  uspreg  21888  ucncn  21899  neipcfilu  21910  cuspusp  21914  isxmet2d  21942  metxmet  21949  xmstps  22068  msxms  22069  xmsxmet  22071  msmet  22072  stdbdxmet  22130  nrgngp  22276  nlmngp  22291  nlmlmod  22292  nlmnrg  22293  nvcnlm  22310  nmoi  22342  nghmrcl1  22346  nghmrcl2  22347  nmhmrcl1  22361  nmhmrcl2  22362  qdensere  22383  xrge0gsumle  22444  xrge0tsms  22445  metds0  22461  metdstri  22462  metdsre  22464  metdseq0  22465  metdscnlem  22466  metnrmlem1a  22469  metnrmlem1  22470  icopnfcnv  22549  cvsclm  22734  cmetmet  22892  cmsms  22953  hlbn  22967  ovolicc2lem5  23096  mblss  23106  mbff  23200  mbfres  23217  mbfadd  23234  mbfsub  23235  i1fmbf  23248  mbfmul  23299  bddmulibl  23411  limcmpt  23453  c1liplem1  23563  c1lip2  23565  fta1glem1  23729  fta1glem2  23730  fta1g  23731  fta1b  23733  ply1pid  23743  aacn  23876  ulmf2  23942  logdmnrp  24187  logdmss  24188  logcnlem2  24189  logcnlem3  24190  logcnlem4  24191  logcnlem5  24192  logcn  24193  dvloglem  24194  logf1o2  24196  efopnlem1  24202  logtayl2  24208  cxpcn  24286  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  atandmneg  24433  atandmcj  24436  cosatan  24448  cosatanne0  24449  birthdaylem1  24478  areacl  24489  cxp2lim  24503  jensenlem2  24514  jensen  24515  sqff1o  24708  dvdsmulf1o  24720  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  lgseisenlem3  24902  chebbnd1  24961  chtppilim  24964  chpchtlim  24968  chpo1ub  24969  dchrmusumlema  24982  dchrvmasumiflem1  24990  dchrisum0lema  25003  dchrisum0lem2  25007  selberg3lem2  25047  pntrsumo1  25054  selbergsb  25064  pnt2  25102  tglineeltr  25326  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  uhgr0vb  25738  uhgra0v  25839  usgra0v  25900  usgra1v  25919  eupagra  26493  frgrawopreg  26576  ablogrpo  26785  bnnv  27106  hlobn  27128  hcauseq  27426  hlimseqi  27430  hlimveci  27431  shss  27451  sh0  27457  chsh  27465  lnopf  28102  bdopln  28104  hmopf  28117  lnfnf  28127  unopf1o  28159  elunop2  28256  elpjhmop  28428  stcltrlem1  28519  mdslle1i  28560  mdslle2i  28561  rabexgfGS  28725  ssnnssfz  28937  tospos  28989  ogrpgrp  29034  ogrpinvOLD  29046  xrge0tsmsd  29116  ofldfld  29141  ofldlt1  29144  ofldchr  29145  isarchiofld  29148  reofld  29171  rearchi  29173  creftop  29241  lmxrge0  29326  qqhrhm  29361  esumpcvgval  29467  dynkin  29557  measssd  29605  elmbfmvol2  29656  omssubadd  29689  sibfinima  29728  eulerpartlemr  29763  eulerpartlemgf  29768  fiblem  29787  domprobmeas  29799  ballotlemscr  29907  ballotlemfg  29914  ballotlemfrc  29915  ballotlemfrceq  29917  ballotlemrinv0  29921  bnj563  30067  bnj658  30075  bnj667  30076  bnj570  30229  bnj938  30261  bnj1001  30282  bnj1006  30283  bnj1049  30296  bnj1121  30307  bnj1173  30324  bnj1177  30328  bnj1245  30336  bnj1311  30346  bnj1321  30349  bnj1388  30355  bnj1398  30356  bnj1415  30360  bnj1417  30363  bnj1421  30364  bnj1442  30371  bnj1452  30374  bnj1489  30378  bnj1312  30380  pcontop  30461  sconpcon  30463  cvmcn  30498  cvmliftlem10  30530  fundmpss  30910  sltres  31061  noseponlem  31065  funpartfun  31220  outsideofcol  31410  fnebas  31509  filnetlem3  31545  phpreu  32563  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  poimirlem26  32605  itg2addnc  32634  istotbnd3  32740  totbndmet  32741  sstotbnd2  32743  sstotbnd  32744  equivtotbnd  32747  bndmet  32750  totbndbnd  32758  prdstotbnd  32763  smgrpismgmOLD  32831  mndoissmgrpOLD  32837  crngorngo  32969  prrngorngo  33020  divrngpr  33022  ollat  33518  omlol  33545  cvlatl  33630  hlomcmcv  33661  2dim  33774  1dimN  33775  lcfl8b  35811  lclkrlem2  35839  lclkrslem1  35844  lclkrslem2  35845  lcfrlem9  35857  mapdval2N  35937  mapdordlem2  35944  mapdrvallem2  35952  nacsacs  36290  eldiophelnn0  36345  lnmlmod  36667  lnrring  36701  mncply  36726  idomrootle  36792  idomodle  36793  areaquad  36821  nznngen  37537  binomcxplemcvg  37575  2uasbanh  37798  fompt  38374  disjinfi  38375  mbfdmssre  38893  stoweidlem14  38907  stoweidlem16  38909  stoweidlem24  38917  stoweidlem51  38944  stoweidlem54  38947  etransclem32  39159  sge0fodjrnlem  39309  preimagelt  39589  preimalegt  39590  pimrecltpos  39596  pimrecltneg  39610  smfaddlem1  39649  ndmafv  39869  evenz  40081  oddz  40082  gbeeven  40176  gboodd  40177  lfuhgr1v0e  40480  nbupgruvtxres  40634  cusgrusgr  40641  frgrusgr  41432  frgrwopreg  41486  rnghmsubcsetclem1  41767  funcrngcsetcALT  41791  rhmsubcsetclem1  41813  rhmsubcrngclem1  41819  ssnn0ssfz  41920  elbigof  42146  digvalnn0  42191