Theorem simplbi 497

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an3  659  xoror  1518  euex  2571  reurex  3360  rabidim1  3431  pssss  4064  eldifi  4097  elinel1  4167  ssunsn2  4794  pwssun  5533  sopo  5568  wefr  5631  opelxp1  5683  relop  5817  ssrelrn  5861  ordtr  6349  funmo  6534  funmoOLD  6535  funrel  6536  fnfun  6621  ffn  6691  f1f  6759  f1of1  6802  f1ofo  6810  isof1o  7301  eqopi  8007  1st2nd2  8010  reldmtpos  8216  brinxper  8703  swoer  8705  ecopover  8797  sdomdom  8954  mapfien  9366  inf3lemd  9587  cardprclem  9939  infxpenlem  9973  cardinfima  10057  dfac5lem4  10086  dfac5lem4OLD  10088  domtriomlem  10402  smobeth  10546  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  axrnegex  11122  axpre-sup  11129  zre  12540  ixxss1  13331  ixxss2  13332  ixxss12  13333  lbioo  13344  ubioo  13345  iccss2  13385  rge0ssre  13424  elfzuz  13488  0wrd0  14512  01sqrexlem6  15220  rlimf  15474  lo1f  15491  lo1dm  15492  o1f  15502  o1dm  15503  mertenslem2  15858  divalglem9  16378  bitsinv2  16420  bitsf1ocnv  16421  gcdcllem1  16476  coprmproddvdslem  16639  prmnn  16651  prmuz2  16673  phimullem  16756  hashgcdlem  16765  1arith  16905  ramtlecl  16978  0ramcl  17001  firest  17402  acsmre  17620  posprs  18284  tospos  18386  latpos  18404  clatpos  18467  dlatl  18490  pslem  18538  tsrlemax  18552  tsrps  18553  sgrpmgm  18658  mndsgrp  18674  grpmnd  18879  nsgsubg  19097  ghmgrp1  19157  ghmgrp2  19158  gimghm  19203  gagrp  19231  gaset  19232  psgneu  19443  efgredeu  19689  ablgrp  19722  cmnmnd  19734  cyggenod2  19822  cyggrp  19827  dprd2dlem1  19980  dprd2da  19981  ablfac2  20028  simpggrp  20033  crngring  20161  dvdsrcl  20281  unitcl  20291  rimrhmOLD  20411  rimrhm  20412  brric2  20422  nzrringOLD  20433  subrgring  20490  subrgrcl  20492  rnghmsubcsetclem1  20547  funcrngcsetcALT  20557  rhmsubcsetclem1  20576  rhmsubcrngclem1  20582  domnnzr  20622  drngring  20652  flddrngd  20657  rng1nfld  20695  srngrhm  20761  lmimlmhm  20978  lveclmod  21020  2idlelbas  21181  rng2idlsubgsubrng  21185  2idlcpblrng  21188  2idlcpbl  21189  qus1  21191  qusrhm  21193  lpirring  21248  cygznlem1  21483  cygznlem3  21486  lbslinds  21749  assalmod  21776  assaring  21777  gsummatr01lem1  22549  topontop  22807  tpstop  22831  mretopd  22986  neiptoptop  23025  perftop  23050  restfpw  23073  cntop1  23134  cntop2  23135  cnptop1  23136  cnptop2  23137  cnprcl  23139  t1ficld  23221  t0top  23223  t1top  23224  haustop  23225  regtop  23227  nrmtop  23230  cnrmtop  23231  pnrmnrm  23234  cmptop  23289  tgcmp  23295  conndisj  23310  conntop  23311  1stctop  23337  llytop  23366  nllytop  23367  hmeocn  23654  filfbas  23742  ufilfil  23798  flimtop  23859  flimfil  23863  alexsublem  23938  ptcmplem3  23948  tsmsfbas  24022  tsmslem1  24023  tsmsgsum  24033  tsmssubm  24037  tsmsres  24038  tsmsf1o  24039  tsmsmhm  24040  tsmsadd  24041  tsmsxplem1  24047  tsmsxplem2  24048  tsmsxp  24049  tlmtmd  24081  tlmlmod  24083  tlmtrg  24084  tvctlm  24091  ressust  24158  uspreg  24168  ucncn  24179  neipcfilu  24190  cuspusp  24194  metxmet  24229  xmstps  24348  msxms  24349  xmsxmet  24351  msmet  24352  nrgngp  24557  nlmngp  24572  nlmlmod  24573  nlmnrg  24574  nvcnlm  24591  nmoi  24623  nghmrcl1  24627  nghmrcl2  24628  nmhmrcl1  24642  nmhmrcl2  24643  qdensere  24664  xrge0gsumle  24729  xrge0tsms  24730  icopnfcnv  24847  cvsclm  25033  cphsscph  25158  cmetmet  25193  cmsms  25255  hlbn  25270  ovolicc2lem5  25429  mblss  25439  mbff  25533  mbfres  25552  i1fmbf  25583  limcmpt  25791  c1liplem1  25908  c1lip2  25910  fta1glem1  26080  fta1glem2  26081  fta1g  26082  fta1b  26084  idomrootle  26085  ply1pid  26095  aacn  26232  ulmf2  26300  logdmnrp  26557  logdmss  26558  logcnlem2  26559  logcnlem3  26560  logcnlem4  26561  logcnlem5  26562  logcn  26563  dvloglem  26564  logf1o2  26566  efopnlem1  26572  logtayl2  26578  cxpcn  26661  cxpcnOLD  26662  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  atandmneg  26823  atandmcj  26826  cosatan  26838  cosatanne0  26839  birthdaylem1  26868  areacl  26879  cxp2lim  26894  jensenlem2  26905  jensen  26906  sqff1o  27099  mpodvdsmulf1o  27111  dvdsmulf1o  27113  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  lgseisenlem3  27295  chebbnd1  27390  chtppilim  27393  chpchtlim  27397  chpo1ub  27398  dchrmusumlema  27411  dchrvmasumiflem1  27419  dchrisum0lema  27432  dchrisum0lem2  27436  selberg3lem2  27476  pntrsumo1  27483  selbergsb  27493  pnt2  27531  sltres  27581  noseponlem  27583  tglineeltr  28565  axcontlem2  28899  axcontlem7  28904  axcontlem8  28905  uhgr0vb  29006  lfuhgr1v0e  29188  fusgrusgr  29256  uvtxisvtx  29323  nbupgruvtxres  29341  cusgrusgr  29353  trliswlk  29632  clwlkiswlk  29711  clwwlkclwwlkn  29966  eupthistrl  30147  frgrusgr  30197  frgrwopreglem5  30257  clwwnonrepclwwnon  30281  ablogrpo  30483  bnnv  30802  hlobn  30824  hcauseq  31121  hlimseqi  31125  hlimveci  31126  shss  31146  sh0  31152  chsh  31160  lnopf  31795  bdopln  31797  hmopf  31810  lnfnf  31820  unopf1o  31852  elunop2  31949  elpjhmop  32121  stcltrlem1  32212  mdslle1i  32253  mdslle2i  32254  2reu2rex1  32417  2reureurex  32418  ssnnssfz  32717  chnwrd  32940  xrge0tsmsd  33009  ogrpgrp  33024  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  isdrng4  33252  ofldfld  33295  ofldlt1  33298  ofldchr  33299  isarchiofld  33302  reofld  33322  rearchi  33324  quslsm  33383  ufdidom  33520  srafldlvec  33589  rgmoddimOLD  33613  extdggt0  33660  fldextid  33662  extdgid  33663  extdgmul  33666  extdg1id  33668  ist0cld  33830  creftop  33843  lmxrge0  33949  qqhrhm  33986  esumpcvgval  34075  dynkin  34164  measssd  34212  elmbfmvol2  34265  omssubadd  34298  sibfinima  34337  eulerpartlemr  34372  eulerpartlemgf  34377  fiblem  34396  domprobmeas  34408  ballotlemscr  34517  ballotlemfg  34524  ballotlemfrc  34525  ballotlemfrceq  34527  ballotlemrinv0  34531  chtvalz  34627  bnj563  34740  bnj658  34748  bnj667  34749  bnj570  34902  bnj938  34934  bnj1001  34956  bnj1006  34957  bnj1049  34971  bnj1121  34982  bnj1173  34999  bnj1177  35003  bnj1245  35011  bnj1311  35021  bnj1321  35024  bnj1388  35030  bnj1398  35031  bnj1415  35035  bnj1417  35038  bnj1421  35039  bnj1442  35046  bnj1452  35049  bnj1489  35053  bnj1312  35055  pthacycspth  35151  pconntop  35219  sconnpconn  35221  cvmcn  35256  cvmliftlem10  35288  sate0fv0  35411  fundmpss  35761  txpss3v  35873  pprodss4v  35879  outsideofcol  36128  fnebas  36339  filnetlem3  36375  bj-nnfe  36726  bj-xpcossxp  37184  bj-rvecmod  37290  pibt2  37412  phpreu  37605  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  poimirlem26  37647  itg2addnc  37675  istotbnd3  37772  totbndmet  37773  sstotbnd2  37775  sstotbnd  37776  equivtotbnd  37779  bndmet  37782  totbndbnd  37790  prdstotbnd  37795  smgrpismgmOLD  37863  mndoissmgrpOLD  37869  crngorngo  38001  prrngorngo  38052  divrngpr  38054  xrnss3v  38361  dfxrn2  38365  refressn  38441  antisymressn  38442  symrelim  38557  eqvrelsym  38603  eqvreltr  38605  disjorimxrn  38747  disjim  38780  disjlem14  38797  ollat  39213  omlol  39240  cvlatl  39325  hlomcmcv  39356  2dim  39471  1dimN  39472  lcfl8b  41505  lclkrlem2  41533  lclkrslem1  41538  lclkrslem2  41539  lcfrlem9  41551  mapdval2N  41631  mapdordlem2  41638  mapdrvallem2  41646  idomnnzgmulnz  42128  aks6d1c6lem3  42167  readvrec2  42356  readvrec  42357  readvcot  42359  nacsacs  42704  eldiophelnn0  42759  lnmlmod  43075  lnrring  43108  mncply  43133  idomodle  43187  areaquad  43212  dfno2  43424  harval3  43534  alephiso3  43555  mnurndlem1  44277  nznngen  44312  binomcxplemcvg  44350  2uasbanh  44558  relpf  44947  disjinfi  45193  climxrre  45755  mbfdmssre  46005  stoweidlem14  46019  stoweidlem16  46021  stoweidlem24  46029  stoweidlem51  46056  stoweidlem54  46059  etransclem32  46271  sge0fodjrnlem  46421  pimrecltpos  46713  pimrecltneg  46729  smfaddlem1  46768  smflimsuplem7  46831  upwordisword  46886  ndmafv  47145  dfafv23  47258  dfatcolem  47260  dfatco  47261  evenz  47635  oddz  47636  gbeeven  47759  gbowodd  47760  sclnbgrisvtx  47853  ssnn0ssfz  48341  elbigof  48547  digvalnn0  48592  2sphere  48742  mof0  48830  mof0ALT  48832  uobeq2  49394  thincc  49415  termcthin  49470