Theorem simplbi 502

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an3  672  xoror  1548  euex  2604  reurex  3371  rabidim1  3436  pssss  4049  eldifi  4081  elinel1  4150  ssunsn2  4791  pwssun  5551  sopo  5586  wefr  5649  opelxp1  5701  relop  5834  ssrelrn  5882  ordtr  6375  funmo  6553  funrel  6554  fnfun  6636  ffn  6706  f1f  6775  f1of1  6820  f1ofo  6829  isof1o  7328  eqopi  8026  1st2nd2  8029  reldmtpos  8236  brinxper  8730  swoer  8732  ecopover  8825  sdomdom  8990  mapfien  9382  inf3lemd  9610  cardprclem  9988  infxpenlem  10020  cardinfima  10104  dfac5lem4  10133  domtriomlem  10448  smobeth  10599  fpwwe2lem5  10648  fpwwe2lem6  10649  fpwwe2lem11  10654  fpwwe2lem12  10655  fpwwe2  10656  axrnegex  11175  axpre-sup  11182  zre  12623  ixxss1  13420  ixxss2  13421  ixxss12  13422  lbioo  13433  ubioo  13434  iccss2  13474  rge0ssre  13513  elfzuz  13578  0wrd0  14609  01sqrexlem6  15338  rlimf  15592  lo1f  15609  lo1dm  15610  o1f  15620  o1dm  15621  mertenslem2  15978  divalglem9  16497  bitsinv2  16539  bitsf1ocnv  16540  gcdcllem1  16595  coprmproddvdslem  16758  prmnn  16770  prmuz2  16792  phimullem  16876  hashgcdlem  16885  1arith  17025  ramtlecl  17098  0ramcl  17121  firest  17523  acsmre  17746  posprs  18410  tospos  18512  latpos  18532  clatpos  18595  dlatl  18618  pslem  18666  tsrlemax  18680  tsrps  18681  chnwrd  18702  sgrpmgm  18832  mndsgrp  18848  grpmnd  19070  nsgsubg  19287  ghmgrp1  19351  ghmgrp2  19352  gimghm  19397  gagrp  19425  gaset  19426  psgneu  19639  efgredeu  19885  ablgrp  19918  cmnmnd  19930  cyggenod2  20018  cyggrp  20023  dprd2dlem1  20176  dprd2da  20177  ablfac2  20224  simpggrp  20229  ogrpgrp  20258  crngring  20390  dvdsrcl  20512  unitcl  20522  rimrhm  20648  isbrric2  20670  nzrringOLD  20683  subrgring  20742  subrgrcl  20744  rnghmsubcsetclem1  20799  funcrngcsetcALT  20809  rhmsubcsetclem1  20828  rhmsubcrngclem1  20834  domnnzr  20874  drngring  20903  isdrng4  20908  flddrngd  20910  rng1nfld  20951  srngrhm  21017  ofldfld  21044  ofldlt1  21047  lmimlmhm  21254  lveclmod  21296  2idlelbas  21472  rng2idlsubgsubrng  21476  2idlcpblrng  21479  2idlcpbl  21480  qus1  21482  qusrhm  21484  lpirring  21568  cygznlem1  21785  cygznlem3  21788  ofldchr  21795  lbslinds  22052  assalmod  22081  assaring  22082  gsummatr01lem1  22883  matunitlindflem1  22907  matunitlindflem2  22908  matunitlindf  22909  topontop  23144  tpstop  23168  mretopd  23323  neiptoptop  23362  perftop  23387  restfpw  23410  cntop1  23471  cntop2  23472  cnptop1  23473  cnptop2  23474  cnprcl  23476  t1ficld  23558  t0top  23560  t1top  23561  haustop  23562  regtop  23564  nrmtop  23567  cnrmtop  23568  pnrmnrm  23571  cmptop  23626  tgcmp  23632  conndisj  23647  conntop  23648  1stctop  23674  llytop  23704  nllytop  23705  hmeocn  23992  filfbas  24080  ufilfil  24136  flimtop  24197  flimfil  24201  alexsublem  24276  ptcmplem3  24286  tsmsfbas  24360  tsmslem1  24361  tsmsgsum  24371  tsmssubm  24375  tsmsres  24376  tsmsf1o  24377  tsmsmhm  24378  tsmsadd  24379  tsmsxplem1  24385  tsmsxplem2  24386  tsmsxp  24387  tlmtmd  24419  tlmlmod  24421  tlmtrg  24422  tvctlm  24429  ressust  24495  uspreg  24505  ucncn  24516  neipcfilu  24527  cuspusp  24531  metxmet  24566  xmstps  24685  msxms  24686  xmsxmet  24688  msmet  24689  nrgngp  24894  nlmngp  24909  nlmlmod  24910  nlmnrg  24911  nvcnlm  24928  nmoi  24960  nghmrcl1  24964  nghmrcl2  24965  nmhmrcl1  24979  nmhmrcl2  24980  qdensere  25001  xrge0gsumle  25066  xrge0tsms  25067  icopnfcnv  25176  cvsclm  25360  cphsscph  25485  cmetmet  25520  cmsms  25582  hlbn  25597  ovolicc2lem5  25755  mblss  25765  mbff  25859  mbfres  25878  i1fmbf  25909  limcmpt  26117  c1liplem1  26230  c1lip2  26232  fta1glem1  26400  fta1glem2  26401  fta1g  26402  fta1b  26404  idomrootle  26405  ply1pid  26415  aacn  26556  ulmf2  26627  logdmnrp  26886  logdmss  26887  logcnlem2  26888  logcnlem3  26889  logcnlem4  26890  logcnlem5  26891  logcn  26892  dvloglem  26893  logf1o2  26895  efopnlem1  26901  logtayl2  26907  cxpcn  26990  cxpcn3lem  26992  cxpcn3  26993  resqrtcn  26994  atandmneg  27151  atandmcj  27154  cosatan  27166  cosatanne0  27167  birthdaylem1  27196  areacl  27207  cxp2lim  27221  jensenlem2  27232  jensen  27233  sqff1o  27426  mpodvdsmulf1o  27438  dvdsmulf1o  27440  lgsqrlem1  27590  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  lgseisenlem3  27621  chebbnd1  27716  chtppilim  27719  chpchtlim  27723  chpo1ub  27724  dchrmusumlema  27737  dchrvmasumiflem1  27745  dchrisum0lema  27758  dchrisum0lem2  27762  selberg3lem2  27802  pntrsumo1  27809  selbergsb  27819  pnt2  27857  ltsres  27906  noseponlem  27908  reno  28765  tglineeltr  28986  axcontlem2  29430  axcontlem7  29435  axcontlem8  29436  uhgr0vb  29537  lfuhgr1v0e  29722  fusgrusgr  29790  uvtxisvtx  29857  nbupgruvtxres  29875  cusgrusgr  29887  trliswlk  30167  clwlkiswlk  30248  clwwlkclwwlkn  30508  eupthistrl  30699  frgrusgr  30749  frgrwopreglem5  30809  clwwnonrepclwwnon  30833  ablogrpo  31036  bnnv  31355  hlobn  31377  hcauseq  31674  hlimseqi  31678  hlimveci  31679  shss  31699  sh0  31705  chsh  31713  lnopf  32348  bdopln  32350  hmopf  32363  lnfnf  32373  unopf1o  32405  elunop2  32502  elpjhmop  32674  stcltrlem1  32765  mdslle1i  32806  mdslle2i  32807  2reu2rex1  32964  2reureurex  32965  ssnnssfz  33266  xrge0tsmsd  33521  isarchiofld  33647  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  reofld  33791  rearchi  33794  quslsm  33842  ufdidom  33960  mplvrpmga  34063  srafldlvec  34104  extdggt0  34175  fldextid  34177  extdgid  34178  extdgmul  34181  extdg1id  34184  ist0cld  34351  creftop  34364  lmxrge0  34470  qqhrhm  34507  esumpcvgval  34596  dynkin  34686  measssd  34734  elmbfmvol2  34786  omssubadd  34819  sibfinima  34858  eulerpartlemr  34893  eulerpartlemgf  34898  fiblem  34917  domprobmeas  34929  ballotlemscr  35038  ballotlemfg  35045  ballotlemfrc  35046  ballotlemfrceq  35048  ballotlemrinv0  35052  chtvalz  35145  bnj563  35261  bnj658  35269  bnj667  35270  bnj570  35422  bnj938  35454  bnj1001  35476  bnj1006  35477  bnj1049  35491  bnj1121  35502  bnj1173  35519  bnj1177  35523  bnj1245  35531  bnj1311  35541  bnj1321  35544  bnj1388  35550  bnj1398  35551  bnj1415  35555  bnj1417  35558  bnj1421  35559  bnj1442  35566  bnj1452  35569  bnj1489  35573  bnj1312  35575  pthacycspth  35744  pconntop  35812  sconnpconn  35814  cvmcn  35849  cvmliftlem10  35881  sate0fv0  36004  fundmpss  36354  txpss3v  36463  pprodss4v  36469  outsideofcol  36721  fnebas  36971  filnetlem3  37007  bj-nnfe  37472  bj-xpcossxp  37949  bj-rvecmod  38055  pibt2  38179  phpreu  38366  poimirlem26  38403  itg2addnc  38431  istotbnd3  38529  totbndmet  38530  sstotbnd2  38532  sstotbnd  38533  equivtotbnd  38536  bndmet  38539  totbndbnd  38547  prdstotbnd  38552  smgrpismgmOLD  38620  mndoissmgrpOLD  38626  crngorngo  38758  prrngorngo  38809  divrngpr  38811  xrnss3v  39137  dfxrn2  39141  refressn  39289  antisymressn  39290  symrelim  39399  eqvrelsym  39445  eqvreltr  39447  disjimeceqim  39560  disjorimxrn  39604  disjim  39640  disjlem14  39657  ollat  40094  omlol  40121  cvlatl  40206  hlomcmcv  40237  2dim  40351  1dimN  40352  lcfl8b  42385  lclkrlem2  42413  lclkrslem1  42418  lclkrslem2  42419  lcfrlem9  42431  mapdval2N  42511  mapdordlem2  42518  mapdrvallem2  42526  idomnnzgmulnz  43007  aks6d1c6lem3  43046  readvrec2  43244  readvrec  43245  readvcot  43247  nacsacs  43562  eldiophelnn0  43617  lnmlmod  43928  lnrring  43961  mncply  43986  idomodle  44040  areaquad  44065  dfno2  44276  harval3  44386  alephiso3  44407  mnurndlem1  45113  nznngen  45148  binomcxplemcvg  45186  2uasbanh  45392  relpf  45781  disjinfi  46032  climxrre  46586  mbfdmssre  46836  stoweidlem14  46850  stoweidlem16  46852  stoweidlem24  46860  stoweidlem51  46887  stoweidlem54  46890  etransclem32  47102  sge0fodjrnlem  47252  pimrecltpos  47544  pimrecltneg  47560  smfaddlem1  47599  smflimsuplem7  47662  chnrin  47732  ndmafv  48036  dfafv23  48149  dfatcolem  48151  dfatco  48152  evenz  48554  oddz  48555  gbeeven  48678  gbowodd  48679  sclnbgrisvtx  48773  grlimgredgex  48924  idomcanr  49271  ssnn0ssfz  49287  elbigof  49492  digvalnn0  49537  2sphere  49687  mof0  49774  mof0ALT  49776  uobeq2  50335  thincc  50356  termcthin  50411