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  2603  reurex  3370  rabidim1  3434  pssss  4046  eldifi  4078  elinel1  4147  ssunsn2  4788  pwssun  5543  sopo  5578  wefr  5641  opelxp1  5693  relop  5828  ssrelrn  5876  ordtr  6369  funmo  6547  funrel  6548  fnfun  6631  ffn  6701  f1f  6770  f1of1  6815  f1ofo  6824  isof1o  7323  eqopi  8026  1st2nd2  8029  reldmtpos  8235  brinxper  8731  swoer  8733  ecopover  8826  sdomdom  8991  mapfien  9384  inf3lemd  9612  cardprclem  10041  infxpenlem  10073  cardinfima  10157  dfac5lem4  10186  domtriomlem  10501  smobeth  10652  fpwwe2lem5  10701  fpwwe2lem6  10702  fpwwe2lem11  10707  fpwwe2lem12  10708  fpwwe2  10709  axrnegex  11228  axpre-sup  11235  zre  12678  ixxss1  13475  ixxss2  13476  ixxss12  13477  lbioo  13488  ubioo  13489  iccss2  13529  rge0ssre  13568  elfzuz  13633  0wrd0  14665  01sqrexlem6  15394  rlimf  15648  lo1f  15665  lo1dm  15666  o1f  15676  o1dm  15677  mertenslem2  16034  divalglem9  16551  bitsinv2  16593  bitsf1ocnv  16594  gcdcllem1  16649  coprmproddvdslem  16817  prmnn  16829  prmuz2  16851  phimullem  16936  hashgcdlem  16945  1arith  17085  ramtlecl  17158  0ramcl  17181  firest  17583  acsmre  17806  posprs  18470  tospos  18572  latpos  18592  clatpos  18655  dlatl  18678  pslem  18726  tsrlemax  18740  tsrps  18741  chnwrd  18762  sgrpmgm  18893  mndsgrp  18909  grpmnd  19131  nsgsubg  19348  ghmgrp1  19412  ghmgrp2  19413  gimghm  19458  gagrp  19486  gaset  19487  psgneu  19700  efgredeu  19946  ablgrp  19979  cmnmnd  19991  cyggenod2  20079  cyggrp  20084  dprd2dlem1  20237  dprd2da  20238  ablfac2  20285  simpggrp  20290  ogrpgrp  20319  crngring  20452  dvdsrcl  20575  unitcl  20585  rimrhm  20711  isbrric2  20733  nzrringOLD  20747  subrgring  20806  subrgrcl  20808  rnghmsubcsetclem1  20863  funcrngcsetcALT  20873  rhmsubcsetclem1  20892  rhmsubcrngclem1  20898  domnnzr  20938  drngring  20967  isdrng4  20972  flddrngd  20974  rng1nfld  21016  srngrhm  21082  ofldfld  21109  ofldlt1  21112  lmimlmhm  21319  lveclmod  21361  2idlelbas  21538  rng2idlsubgsubrng  21542  2idlcpblrng  21545  2idlcpbl  21546  qus1  21548  qusrhm  21550  lpirring  21635  cygznlem1  21852  cygznlem3  21855  ofldchr  21862  lbslinds  22119  assalmod  22148  assaring  22149  gsummatr01lem1  22950  matunitlindflem1  22974  matunitlindflem2  22975  matunitlindf  22976  topontop  23211  tpstop  23235  mretopd  23390  neiptoptop  23429  perftop  23454  restfpw  23477  cntop1  23538  cntop2  23539  cnptop1  23540  cnptop2  23541  cnprcl  23543  t1ficld  23625  t0top  23627  t1top  23628  haustop  23629  regtop  23631  nrmtop  23634  cnrmtop  23635  pnrmnrm  23638  cmptop  23693  tgcmp  23699  conndisj  23714  conntop  23715  1stctop  23741  llytop  23771  nllytop  23772  hmeocn  24059  filfbas  24147  ufilfil  24203  flimtop  24264  flimfil  24268  alexsublem  24343  ptcmplem3  24353  tsmsfbas  24427  tsmslem1  24428  tsmsgsum  24438  tsmssubm  24442  tsmsres  24443  tsmsf1o  24444  tsmsmhm  24445  tsmsadd  24446  tsmsxplem1  24452  tsmsxplem2  24453  tsmsxp  24454  tlmtmd  24486  tlmlmod  24488  tlmtrg  24489  tvctlm  24496  ressust  24562  uspreg  24572  ucncn  24583  neipcfilu  24594  cuspusp  24598  metxmet  24633  xmstps  24752  msxms  24753  xmsxmet  24755  msmet  24756  nrgngp  24961  nlmngp  24976  nlmlmod  24977  nlmnrg  24978  nvcnlm  24995  nmoi  25027  nghmrcl1  25031  nghmrcl2  25032  nmhmrcl1  25046  nmhmrcl2  25047  qdensere  25068  xrge0gsumle  25133  xrge0tsms  25134  icopnfcnv  25243  cvsclm  25427  cphsscph  25552  cmetmet  25587  cmsms  25649  hlbn  25664  ovolicc2lem5  25822  mblss  25832  mbff  25926  mbfres  25945  i1fmbf  25976  limcmpt  26183  c1liplem1  26296  c1lip2  26298  fta1glem1  26466  fta1glem2  26467  fta1g  26468  fta1b  26470  idomrootle  26471  ply1pid  26481  aacn  26622  ulmf2  26693  logdmnrp  26951  logdmss  26952  logcnlem2  26953  logcnlem3  26954  logcnlem4  26955  logcnlem5  26956  logcn  26957  dvloglem  26958  logf1o2  26960  efopnlem1  26966  logtayl2  26972  cxpcn  27055  cxpcn3lem  27057  cxpcn3  27058  resqrtcn  27059  atandmneg  27216  atandmcj  27219  cosatan  27231  cosatanne0  27232  birthdaylem1  27261  areacl  27272  cxp2lim  27286  jensenlem2  27297  jensen  27298  sqff1o  27491  mpodvdsmulf1o  27503  dvdsmulf1o  27505  lgsqrlem1  27655  lgsqrlem2  27656  lgsqrlem3  27657  lgsqrlem4  27658  lgseisenlem3  27686  chebbnd1  27781  chtppilim  27784  chpchtlim  27788  chpo1ub  27789  dchrmusumlema  27802  dchrvmasumiflem1  27810  dchrisum0lema  27823  dchrisum0lem2  27827  selberg3lem2  27867  pntrsumo1  27874  selbergsb  27884  pnt2  27922  ltsres  28001  noseponlem  28003  reno  28860  tglineeltr  29081  axcontlem2  29525  axcontlem7  29530  axcontlem8  29531  uhgr0vb  29632  lfuhgr1v0e  29817  fusgrusgr  29885  uvtxisvtx  29952  nbupgruvtxres  29970  cusgrusgr  29982  trliswlk  30262  clwlkiswlk  30343  clwwlkclwwlkn  30603  eupthistrl  30794  frgrusgr  30844  frgrwopreglem5  30904  clwwnonrepclwwnon  30928  ablogrpo  31131  bnnv  31450  hlobn  31472  hcauseq  31769  hlimseqi  31773  hlimveci  31774  shss  31794  sh0  31800  chsh  31808  lnopf  32443  bdopln  32445  hmopf  32458  lnfnf  32468  unopf1o  32500  elunop2  32597  elpjhmop  32769  stcltrlem1  32860  mdslle1i  32901  mdslle2i  32902  2reu2rex1  33059  2reureurex  33060  ssnnssfz  33361  xrge0tsmsd  33616  isarchiofld  33742  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem4  33788  reofld  33886  rearchi  33889  quslsm  33938  ufdidom  34056  mplvrpmga  34159  srafldlvec  34200  extdggt0  34271  fldextid  34273  extdgid  34274  extdgmul  34277  extdg1id  34280  ist0cld  34447  creftop  34460  lmxrge0  34566  qqhrhm  34603  esumpcvgval  34692  dynkin  34782  measssd  34830  elmbfmvol2  34882  omssubadd  34915  sibfinima  34954  eulerpartlemr  34989  eulerpartlemgf  34994  fiblem  35013  domprobmeas  35025  ballotlemscr  35134  ballotlemfg  35141  ballotlemfrc  35142  ballotlemfrceq  35144  ballotlemrinv0  35148  chtvalz  35241  bnj563  35357  bnj658  35365  bnj667  35366  bnj570  35518  bnj938  35550  bnj1001  35572  bnj1006  35573  bnj1049  35587  bnj1121  35598  bnj1173  35615  bnj1177  35619  bnj1245  35627  bnj1311  35637  bnj1321  35640  bnj1388  35646  bnj1398  35647  bnj1415  35651  bnj1417  35654  bnj1421  35655  bnj1442  35662  bnj1452  35665  bnj1489  35669  bnj1312  35671  pthacycspth  35891  pconntop  35959  sconnpconn  35961  cvmcn  35996  cvmliftlem10  36028  sate0fv0  36151  fundmpss  36501  txpss3v  36610  pprodss4v  36616  outsideofcol  36868  fnebas  37102  filnetlem3  37138  bj-nnfe  37603  bj-xpcossxp  38078  bj-rvecmod  38184  pibt2  38308  phpreu  38495  poimirlem26  38532  itg2addnc  38560  istotbnd3  38673  totbndmet  38674  sstotbnd2  38676  sstotbnd  38677  equivtotbnd  38680  bndmet  38683  totbndbnd  38691  prdstotbnd  38696  smgrpismgmOLD  38764  mndoissmgrpOLD  38770  crngorngo  38902  prrngorngo  38953  divrngpr  38955  xrnss3v  39281  dfxrn2  39285  refressn  39433  antisymressn  39434  symrelim  39543  eqvrelsym  39589  eqvreltr  39591  disjimeceqim  39704  disjorimxrn  39748  disjim  39784  disjlem14  39801  ollat  40238  omlol  40265  cvlatl  40350  hlomcmcv  40381  2dim  40495  1dimN  40496  lcfl8b  42529  lclkrlem2  42557  lclkrslem1  42562  lclkrslem2  42563  lcfrlem9  42575  mapdval2N  42655  mapdordlem2  42662  mapdrvallem2  42670  idomnnzgmulnz  43151  aks6d1c6lem3  43190  readvrec2  43380  readvrec  43381  readvcot  43383  nacsacs  43673  eldiophelnn0  43728  lnmlmod  44039  lnrring  44072  mncply  44097  idomodle  44151  areaquad  44176  dfno2  44387  harval3  44497  alephiso3  44518  mnurndlem1  45224  nznngen  45259  binomcxplemcvg  45297  2uasbanh  45503  relpf  45892  disjinfi  46150  climxrre  46704  mbfdmssre  46954  stoweidlem14  46968  stoweidlem16  46970  stoweidlem24  46978  stoweidlem51  47005  stoweidlem54  47008  etransclem32  47220  sge0fodjrnlem  47370  pimrecltpos  47662  pimrecltneg  47678  smfaddlem1  47717  smflimsuplem7  47780  chnrin  47850  ndmafv  48154  dfafv23  48267  dfatcolem  48269  dfatco  48270  evenz  48672  oddz  48673  gbeeven  48796  gbowodd  48797  sclnbgrisvtx  48891  grlimgredgex  49042  idomcanr  49389  ssnn0ssfz  49405  elbigof  49610  digvalnn0  49655  2sphere  49805  mof0  49892  mof0ALT  49894  uobeq2  50453  thinccat  50474  termcthin  50529