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  1514  euex  2574  reurex  3381  rabidim1  3455  pssss  4107  eldifi  4140  elinel1  4210  ssunsn2  4831  pwssun  5579  sopo  5615  wefr  5678  opelxp1  5730  relop  5863  ssrelrn  5907  ordtr  6399  funmo  6582  funmoOLD  6583  funrel  6584  fnfun  6668  ffn  6736  f1f  6804  f1of1  6847  f1ofo  6855  isof1o  7342  eqopi  8048  1st2nd2  8051  reldmtpos  8257  brinxper  8772  swoer  8774  ecopover  8859  sdomdom  9018  mapfien  9445  inf3lemd  9664  cardprclem  10016  infxpenlem  10050  cardinfima  10134  dfac5lem4  10163  dfac5lem4OLD  10165  domtriomlem  10479  smobeth  10623  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  axrnegex  11199  axpre-sup  11206  zre  12614  ixxss1  13401  ixxss2  13402  ixxss12  13403  lbioo  13414  ubioo  13415  iccss2  13454  rge0ssre  13492  elfzuz  13556  0wrd0  14574  01sqrexlem6  15282  rlimf  15533  lo1f  15550  lo1dm  15551  o1f  15561  o1dm  15562  mertenslem2  15917  divalglem9  16434  bitsinv2  16476  bitsf1ocnv  16477  gcdcllem1  16532  coprmproddvdslem  16695  prmnn  16707  prmuz2  16729  phimullem  16812  hashgcdlem  16821  1arith  16960  ramtlecl  17033  0ramcl  17056  firest  17478  acsmre  17696  posprs  18373  tospos  18477  latpos  18495  clatpos  18558  dlatl  18581  pslem  18629  tsrlemax  18643  tsrps  18644  sgrpmgm  18749  mndsgrp  18765  grpmnd  18970  nsgsubg  19188  ghmgrp1  19248  ghmgrp2  19249  gimghm  19294  gagrp  19322  gaset  19323  psgneu  19538  efgredeu  19784  ablgrp  19817  cmnmnd  19829  cyggenod2  19917  cyggrp  19922  dprd2dlem1  20075  dprd2da  20076  ablfac2  20123  simpggrp  20128  crngring  20262  dvdsrcl  20381  unitcl  20391  rimrhmOLD  20511  rimrhm  20512  brric2  20522  nzrringOLD  20533  subrgring  20590  subrgrcl  20592  rnghmsubcsetclem1  20647  funcrngcsetcALT  20657  rhmsubcsetclem1  20676  rhmsubcrngclem1  20682  domnnzr  20722  drngring  20752  flddrngd  20757  fldidomOLD  20788  rng1nfld  20796  srngrhm  20862  lmimlmhm  21080  lveclmod  21122  2idlelbas  21291  rng2idlsubgsubrng  21295  2idlcpblrng  21298  2idlcpbl  21299  qus1  21301  qusrhm  21303  lpirring  21358  cygznlem1  21602  cygznlem3  21605  lbslinds  21870  assalmod  21897  assaring  21898  gsummatr01lem1  22676  topontop  22934  tpstop  22958  mretopd  23115  neiptoptop  23154  perftop  23179  restfpw  23202  cntop1  23263  cntop2  23264  cnptop1  23265  cnptop2  23266  cnprcl  23268  t1ficld  23350  t0top  23352  t1top  23353  haustop  23354  regtop  23356  nrmtop  23359  cnrmtop  23360  pnrmnrm  23363  cmptop  23418  tgcmp  23424  conndisj  23439  conntop  23440  1stctop  23466  llytop  23495  nllytop  23496  hmeocn  23783  filfbas  23871  ufilfil  23927  flimtop  23988  flimfil  23992  alexsublem  24067  ptcmplem3  24077  tsmsfbas  24151  tsmslem1  24152  tsmsgsum  24162  tsmssubm  24166  tsmsres  24167  tsmsf1o  24168  tsmsmhm  24169  tsmsadd  24170  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  tlmtmd  24210  tlmlmod  24212  tlmtrg  24213  tvctlm  24220  ressust  24287  uspreg  24298  ucncn  24309  neipcfilu  24320  cuspusp  24324  metxmet  24359  xmstps  24478  msxms  24479  xmsxmet  24481  msmet  24482  nrgngp  24698  nlmngp  24713  nlmlmod  24714  nlmnrg  24715  nvcnlm  24732  nmoi  24764  nghmrcl1  24768  nghmrcl2  24769  nmhmrcl1  24783  nmhmrcl2  24784  qdensere  24805  xrge0gsumle  24868  xrge0tsms  24869  icopnfcnv  24986  cvsclm  25172  cphsscph  25298  cmetmet  25333  cmsms  25395  hlbn  25410  ovolicc2lem5  25569  mblss  25579  mbff  25673  mbfres  25692  i1fmbf  25723  limcmpt  25932  c1liplem1  26049  c1lip2  26051  fta1glem1  26221  fta1glem2  26222  fta1g  26223  fta1b  26225  idomrootle  26226  ply1pid  26236  aacn  26373  ulmf2  26441  logdmnrp  26697  logdmss  26698  logcnlem2  26699  logcnlem3  26700  logcnlem4  26701  logcnlem5  26702  logcn  26703  dvloglem  26704  logf1o2  26706  efopnlem1  26712  logtayl2  26718  cxpcn  26801  cxpcnOLD  26802  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  atandmneg  26963  atandmcj  26966  cosatan  26978  cosatanne0  26979  birthdaylem1  27008  areacl  27019  cxp2lim  27034  jensenlem2  27045  jensen  27046  sqff1o  27239  mpodvdsmulf1o  27251  dvdsmulf1o  27253  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  lgseisenlem3  27435  chebbnd1  27530  chtppilim  27533  chpchtlim  27537  chpo1ub  27538  dchrmusumlema  27551  dchrvmasumiflem1  27559  dchrisum0lema  27572  dchrisum0lem2  27576  selberg3lem2  27616  pntrsumo1  27623  selbergsb  27633  pnt2  27671  sltres  27721  noseponlem  27723  tglineeltr  28653  axcontlem2  28994  axcontlem7  28999  axcontlem8  29000  uhgr0vb  29103  lfuhgr1v0e  29285  fusgrusgr  29353  uvtxisvtx  29420  nbupgruvtxres  29438  cusgrusgr  29450  trliswlk  29729  clwlkiswlk  29806  clwwlkclwwlkn  30058  eupthistrl  30239  frgrusgr  30289  frgrwopreglem5  30349  clwwnonrepclwwnon  30373  ablogrpo  30575  bnnv  30894  hlobn  30916  hcauseq  31213  hlimseqi  31217  hlimveci  31218  shss  31238  sh0  31244  chsh  31252  lnopf  31887  bdopln  31889  hmopf  31902  lnfnf  31912  unopf1o  31944  elunop2  32041  elpjhmop  32213  stcltrlem1  32304  mdslle1i  32345  mdslle2i  32346  2reu2rex1  32508  2reureurex  32509  ssnnssfz  32795  chnwrd  32981  xrge0tsmsd  33047  ogrpgrp  33062  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  isdrng4  33278  ofldfld  33319  ofldlt1  33322  ofldchr  33323  isarchiofld  33326  reofld  33351  rearchi  33353  quslsm  33412  ufdidom  33549  srafldlvec  33615  rgmoddimOLD  33637  extdggt0  33684  fldextid  33686  extdgid  33687  extdgmul  33688  extdg1id  33690  ist0cld  33793  creftop  33806  lmxrge0  33912  qqhrhm  33951  esumpcvgval  34058  dynkin  34147  measssd  34195  elmbfmvol2  34248  omssubadd  34281  sibfinima  34320  eulerpartlemr  34355  eulerpartlemgf  34360  fiblem  34379  domprobmeas  34391  ballotlemscr  34499  ballotlemfg  34506  ballotlemfrc  34507  ballotlemfrceq  34509  ballotlemrinv0  34513  chtvalz  34622  bnj563  34735  bnj658  34743  bnj667  34744  bnj570  34897  bnj938  34929  bnj1001  34951  bnj1006  34952  bnj1049  34966  bnj1121  34977  bnj1173  34994  bnj1177  34998  bnj1245  35006  bnj1311  35016  bnj1321  35019  bnj1388  35025  bnj1398  35026  bnj1415  35030  bnj1417  35033  bnj1421  35034  bnj1442  35041  bnj1452  35044  bnj1489  35048  bnj1312  35050  pthacycspth  35141  pconntop  35209  sconnpconn  35211  cvmcn  35246  cvmliftlem10  35278  sate0fv0  35401  fundmpss  35747  txpss3v  35859  pprodss4v  35865  outsideofcol  36114  fnebas  36326  filnetlem3  36362  bj-nnfe  36713  bj-xpcossxp  37171  bj-rvecmod  37277  pibt2  37399  phpreu  37590  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  poimirlem26  37632  itg2addnc  37660  istotbnd3  37757  totbndmet  37758  sstotbnd2  37760  sstotbnd  37761  equivtotbnd  37764  bndmet  37767  totbndbnd  37775  prdstotbnd  37780  smgrpismgmOLD  37848  mndoissmgrpOLD  37854  crngorngo  37986  prrngorngo  38037  divrngpr  38039  xrnss3v  38353  dfxrn2  38357  refressn  38424  antisymressn  38425  symrelim  38540  eqvrelsym  38586  eqvreltr  38588  disjorimxrn  38729  disjim  38762  disjlem14  38779  ollat  39194  omlol  39221  cvlatl  39306  hlomcmcv  39337  2dim  39452  1dimN  39453  lcfl8b  41486  lclkrlem2  41514  lclkrslem1  41519  lclkrslem2  41520  lcfrlem9  41532  mapdval2N  41612  mapdordlem2  41619  mapdrvallem2  41627  idomnnzgmulnz  42114  aks6d1c6lem3  42153  readvrec2  42369  readvrec  42370  nacsacs  42696  eldiophelnn0  42751  lnmlmod  43067  lnrring  43100  mncply  43125  idomodle  43179  areaquad  43204  dfno2  43417  harval3  43527  alephiso3  43548  mnurndlem1  44276  nznngen  44311  binomcxplemcvg  44349  2uasbanh  44558  disjinfi  45134  climxrre  45705  mbfdmssre  45955  stoweidlem14  45969  stoweidlem16  45971  stoweidlem24  45979  stoweidlem51  46006  stoweidlem54  46009  etransclem32  46221  sge0fodjrnlem  46371  pimrecltpos  46663  pimrecltneg  46679  smfaddlem1  46718  smflimsuplem7  46781  upwordisword  46834  ndmafv  47089  dfafv23  47202  dfatcolem  47204  dfatco  47205  evenz  47554  oddz  47555  gbeeven  47678  gbowodd  47679  sclnbgrisvtx  47772  ssnn0ssfz  48193  elbigof  48403  digvalnn0  48448  2sphere  48598  mof0  48667  mof0ALT  48669  thincc  48823