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  2608  reurex  3376  rabidim1  3441  pssss  4055  eldifi  4088  elinel1  4157  ssunsn2  4798  pwssun  5558  sopo  5593  wefr  5656  opelxp1  5708  relop  5841  ssrelrn  5889  ordtr  6381  funmo  6559  funrel  6560  fnfun  6642  ffn  6712  f1f  6781  f1of1  6826  f1ofo  6835  isof1o  7332  eqopi  8031  1st2nd2  8034  reldmtpos  8239  brinxper  8733  swoer  8735  ecopover  8828  sdomdom  8986  mapfien  9378  inf3lemd  9606  cardprclem  9984  infxpenlem  10016  cardinfima  10100  dfac5lem4  10129  domtriomlem  10444  smobeth  10589  fpwwe2lem5  10638  fpwwe2lem6  10639  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  axrnegex  11165  axpre-sup  11172  zre  12613  ixxss1  13408  ixxss2  13409  ixxss12  13410  lbioo  13421  ubioo  13422  iccss2  13462  rge0ssre  13501  elfzuz  13566  0wrd0  14597  01sqrexlem6  15324  rlimf  15578  lo1f  15595  lo1dm  15596  o1f  15606  o1dm  15607  mertenslem2  15965  divalglem9  16484  bitsinv2  16526  bitsf1ocnv  16527  gcdcllem1  16582  coprmproddvdslem  16745  prmnn  16757  prmuz2  16779  phimullem  16863  hashgcdlem  16872  1arith  17012  ramtlecl  17085  0ramcl  17108  firest  17510  acsmre  17733  posprs  18397  tospos  18499  latpos  18519  clatpos  18582  dlatl  18605  pslem  18653  tsrlemax  18667  tsrps  18668  chnwrd  18689  sgrpmgm  18811  mndsgrp  18827  grpmnd  19038  nsgsubg  19255  ghmgrp1  19319  ghmgrp2  19320  gimghm  19365  gagrp  19393  gaset  19394  psgneu  19607  efgredeu  19853  ablgrp  19886  cmnmnd  19898  cyggenod2  19986  cyggrp  19991  dprd2dlem1  20144  dprd2da  20145  ablfac2  20192  simpggrp  20197  ogrpgrp  20226  crngring  20358  dvdsrcl  20480  unitcl  20490  rimrhm  20616  isbrric2  20638  nzrringOLD  20651  subrgring  20710  subrgrcl  20712  rnghmsubcsetclem1  20767  funcrngcsetcALT  20777  rhmsubcsetclem1  20796  rhmsubcrngclem1  20802  domnnzr  20842  drngring  20871  isdrng4  20876  flddrngd  20878  rng1nfld  20919  srngrhm  20985  ofldfld  21012  ofldlt1  21015  lmimlmhm  21222  lveclmod  21264  2idlelbas  21440  rng2idlsubgsubrng  21444  2idlcpblrng  21447  2idlcpbl  21448  qus1  21450  qusrhm  21452  lpirring  21536  cygznlem1  21753  cygznlem3  21756  ofldchr  21763  lbslinds  22020  assalmod  22047  assaring  22048  gsummatr01lem1  22849  topontop  23107  tpstop  23131  mretopd  23286  neiptoptop  23325  perftop  23350  restfpw  23373  cntop1  23434  cntop2  23435  cnptop1  23436  cnptop2  23437  cnprcl  23439  t1ficld  23521  t0top  23523  t1top  23524  haustop  23525  regtop  23527  nrmtop  23530  cnrmtop  23531  pnrmnrm  23534  cmptop  23589  tgcmp  23595  conndisj  23610  conntop  23611  1stctop  23637  llytop  23666  nllytop  23667  hmeocn  23954  filfbas  24042  ufilfil  24098  flimtop  24159  flimfil  24163  alexsublem  24238  ptcmplem3  24248  tsmsfbas  24322  tsmslem1  24323  tsmsgsum  24333  tsmssubm  24337  tsmsres  24338  tsmsf1o  24339  tsmsmhm  24340  tsmsadd  24341  tsmsxplem1  24347  tsmsxplem2  24348  tsmsxp  24349  tlmtmd  24381  tlmlmod  24383  tlmtrg  24384  tvctlm  24391  ressust  24457  uspreg  24467  ucncn  24478  neipcfilu  24489  cuspusp  24493  metxmet  24528  xmstps  24647  msxms  24648  xmsxmet  24650  msmet  24651  nrgngp  24856  nlmngp  24871  nlmlmod  24872  nlmnrg  24873  nvcnlm  24890  nmoi  24922  nghmrcl1  24926  nghmrcl2  24927  nmhmrcl1  24941  nmhmrcl2  24942  qdensere  24963  xrge0gsumle  25028  xrge0tsms  25029  icopnfcnv  25138  cvsclm  25322  cphsscph  25447  cmetmet  25482  cmsms  25544  hlbn  25559  ovolicc2lem5  25717  mblss  25727  mbff  25821  mbfres  25840  i1fmbf  25871  limcmpt  26079  c1liplem1  26192  c1lip2  26194  fta1glem1  26362  fta1glem2  26363  fta1g  26364  fta1b  26366  idomrootle  26367  ply1pid  26377  aacn  26515  ulmf2  26584  logdmnrp  26843  logdmss  26844  logcnlem2  26845  logcnlem3  26846  logcnlem4  26847  logcnlem5  26848  logcn  26849  dvloglem  26850  logf1o2  26852  efopnlem1  26858  logtayl2  26864  cxpcn  26947  cxpcn3lem  26949  cxpcn3  26950  resqrtcn  26951  atandmneg  27108  atandmcj  27111  cosatan  27123  cosatanne0  27124  birthdaylem1  27153  areacl  27164  cxp2lim  27178  jensenlem2  27189  jensen  27190  sqff1o  27383  mpodvdsmulf1o  27395  dvdsmulf1o  27397  lgsqrlem1  27547  lgsqrlem2  27548  lgsqrlem3  27549  lgsqrlem4  27550  lgseisenlem3  27578  chebbnd1  27673  chtppilim  27676  chpchtlim  27680  chpo1ub  27681  dchrmusumlema  27694  dchrvmasumiflem1  27702  dchrisum0lema  27715  dchrisum0lem2  27719  selberg3lem2  27759  pntrsumo1  27766  selbergsb  27776  pnt2  27814  ltsres  27863  noseponlem  27865  reno  28722  tglineeltr  28941  axcontlem2  29352  axcontlem7  29357  axcontlem8  29358  uhgr0vb  29459  lfuhgr1v0e  29641  fusgrusgr  29709  uvtxisvtx  29776  nbupgruvtxres  29794  cusgrusgr  29806  trliswlk  30082  clwlkiswlk  30160  clwwlkclwwlkn  30418  eupthistrl  30599  frgrusgr  30649  frgrwopreglem5  30709  clwwnonrepclwwnon  30733  ablogrpo  30936  bnnv  31255  hlobn  31277  hcauseq  31574  hlimseqi  31578  hlimveci  31579  shss  31599  sh0  31605  chsh  31613  lnopf  32248  bdopln  32250  hmopf  32263  lnfnf  32273  unopf1o  32305  elunop2  32402  elpjhmop  32574  stcltrlem1  32665  mdslle1i  32706  mdslle2i  32707  2reu2rex1  32864  2reureurex  32865  ssnnssfz  33169  xrge0tsmsd  33424  isarchiofld  33550  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem4  33596  reofld  33694  rearchi  33697  quslsm  33745  ufdidom  33863  mplvrpmga  33966  srafldlvec  34007  extdggt0  34078  fldextid  34080  extdgid  34081  extdgmul  34084  extdg1id  34087  ist0cld  34254  creftop  34267  lmxrge0  34373  qqhrhm  34410  esumpcvgval  34499  dynkin  34589  measssd  34637  elmbfmvol2  34689  omssubadd  34722  sibfinima  34761  eulerpartlemr  34796  eulerpartlemgf  34801  fiblem  34820  domprobmeas  34832  ballotlemscr  34941  ballotlemfg  34948  ballotlemfrc  34949  ballotlemfrceq  34951  ballotlemrinv0  34955  chtvalz  35048  bnj563  35164  bnj658  35172  bnj667  35173  bnj570  35325  bnj938  35357  bnj1001  35379  bnj1006  35380  bnj1049  35394  bnj1121  35405  bnj1173  35422  bnj1177  35426  bnj1245  35434  bnj1311  35444  bnj1321  35447  bnj1388  35453  bnj1398  35454  bnj1415  35458  bnj1417  35461  bnj1421  35462  bnj1442  35469  bnj1452  35472  bnj1489  35476  bnj1312  35478  pthacycspth  35670  pconntop  35738  sconnpconn  35740  cvmcn  35775  cvmliftlem10  35807  sate0fv0  35930  fundmpss  36280  txpss3v  36389  pprodss4v  36395  outsideofcol  36646  fnebas  36896  filnetlem3  36932  bj-nnfe  37397  bj-xpcossxp  37874  bj-rvecmod  37980  pibt2  38104  phpreu  38296  matunitlindflem1  38308  matunitlindflem2  38309  matunitlindf  38310  poimirlem26  38338  itg2addnc  38366  istotbnd3  38463  totbndmet  38464  sstotbnd2  38466  sstotbnd  38467  equivtotbnd  38470  bndmet  38473  totbndbnd  38481  prdstotbnd  38486  smgrpismgmOLD  38554  mndoissmgrpOLD  38560  crngorngo  38692  prrngorngo  38743  divrngpr  38745  xrnss3v  39071  dfxrn2  39075  refressn  39223  antisymressn  39224  symrelim  39333  eqvrelsym  39379  eqvreltr  39381  disjimeceqim  39494  disjorimxrn  39538  disjim  39574  disjlem14  39591  ollat  40028  omlol  40055  cvlatl  40140  hlomcmcv  40171  2dim  40285  1dimN  40286  lcfl8b  42319  lclkrlem2  42347  lclkrslem1  42352  lclkrslem2  42353  lcfrlem9  42365  mapdval2N  42445  mapdordlem2  42452  mapdrvallem2  42460  idomnnzgmulnz  42941  aks6d1c6lem3  42980  readvrec2  43163  readvrec  43164  readvcot  43166  nacsacs  43481  eldiophelnn0  43536  lnmlmod  43847  lnrring  43880  mncply  43905  idomodle  43959  areaquad  43984  dfno2  44195  harval3  44305  alephiso3  44326  mnurndlem1  45032  nznngen  45067  binomcxplemcvg  45105  2uasbanh  45311  relpf  45700  disjinfi  45951  climxrre  46505  mbfdmssre  46755  stoweidlem14  46769  stoweidlem16  46771  stoweidlem24  46779  stoweidlem51  46806  stoweidlem54  46809  etransclem32  47021  sge0fodjrnlem  47171  pimrecltpos  47463  pimrecltneg  47479  smfaddlem1  47518  smflimsuplem7  47581  ndmafv  47918  dfafv23  48031  dfatcolem  48033  dfatco  48034  evenz  48436  oddz  48437  gbeeven  48560  gbowodd  48561  sclnbgrisvtx  48655  grlimgredgex  48806  idomcanr  49154  ssnn0ssfz  49170  elbigof  49375  digvalnn0  49420  2sphere  49570  mof0  49657  mof0ALT  49659  uobeq2  50220  thincc  50241  termcthin  50296