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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  an3  656  xoror  1511  euex  2563  reurex  3372  rabidim1  3445  pssss  4087  eldifi  4118  elinel1  4187  ssunsn2  4822  pwssun  5561  sopo  5597  wefr  5656  opelxp1  5708  relop  5840  ssrelrn  5884  ordtr  6368  funmo  6553  funmoOLD  6554  funrel  6555  fnfun  6639  ffn  6707  f1f  6777  f1of1  6822  f1ofo  6830  isof1o  7312  eqopi  8004  1st2nd2  8007  reldmtpos  8214  swoer  8728  ecopover  8810  sdomdom  8971  mapfien  9398  inf3lemd  9617  cardprclem  9969  infxpenlem  10003  cardinfima  10087  dfac5lem4  10116  domtriomlem  10432  smobeth  10576  fpwwe2lem5  10625  fpwwe2lem6  10626  fpwwe2lem11  10631  fpwwe2lem12  10632  fpwwe2  10633  axrnegex  11152  axpre-sup  11159  zre  12558  ixxss1  13338  ixxss2  13339  ixxss12  13340  lbioo  13351  ubioo  13352  iccss2  13391  rge0ssre  13429  elfzuz  13493  0wrd0  14486  01sqrexlem6  15190  rlimf  15441  lo1f  15458  lo1dm  15459  o1f  15469  o1dm  15470  mertenslem2  15827  divalglem9  16340  bitsinv2  16380  bitsf1ocnv  16381  gcdcllem1  16436  coprmproddvdslem  16595  prmnn  16607  prmuz2  16629  phimullem  16710  hashgcdlem  16719  1arith  16858  ramtlecl  16931  0ramcl  16954  firest  17376  acsmre  17594  posprs  18270  tospos  18374  latpos  18392  clatpos  18455  dlatl  18478  pslem  18526  tsrlemax  18540  tsrps  18541  sgrpmgm  18646  mndsgrp  18662  grpmnd  18859  nsgsubg  19074  ghmgrp1  19132  ghmgrp2  19133  gimghm  19178  gagrp  19197  gaset  19198  psgneu  19415  efgredeu  19661  ablgrp  19694  cmnmnd  19706  cyggenod2  19794  cyggrp  19799  dprd2dlem1  19952  dprd2da  19953  ablfac2  20000  simpggrp  20005  crngring  20139  dvdsrcl  20256  unitcl  20266  rimrhmOLD  20386  rimrhm  20387  brric2  20397  nzrringOLD  20408  subrgring  20465  subrgrcl  20467  rnghmsubcsetclem1  20516  funcrngcsetcALT  20526  rhmsubcsetclem1  20545  rhmsubcrngclem1  20551  drngring  20583  flddrngd  20588  rng1nfld  20619  srngrhm  20683  lmimlmhm  20901  lveclmod  20943  2idlelbas  21110  rng2idlsubgsubrng  21114  2idlcpblrng  21117  2idlcpbl  21118  qus1  21120  qusrhm  21122  lpirring  21173  domnnzr  21194  fldidomOLD  21207  cygznlem1  21428  cygznlem3  21431  lbslinds  21695  assalmod  21722  assaring  21723  gsummatr01lem1  22478  topontop  22736  tpstop  22760  mretopd  22917  neiptoptop  22956  perftop  22981  restfpw  23004  cntop1  23065  cntop2  23066  cnptop1  23067  cnptop2  23068  cnprcl  23070  t1ficld  23152  t0top  23154  t1top  23155  haustop  23156  regtop  23158  nrmtop  23161  cnrmtop  23162  pnrmnrm  23165  cmptop  23220  tgcmp  23226  conndisj  23241  conntop  23242  1stctop  23268  llytop  23297  nllytop  23298  hmeocn  23585  filfbas  23673  ufilfil  23729  flimtop  23790  flimfil  23794  alexsublem  23869  ptcmplem3  23879  tsmsfbas  23953  tsmslem1  23954  tsmsgsum  23964  tsmssubm  23968  tsmsres  23969  tsmsf1o  23970  tsmsmhm  23971  tsmsadd  23972  tsmsxplem1  23978  tsmsxplem2  23979  tsmsxp  23980  tlmtmd  24012  tlmlmod  24014  tlmtrg  24015  tvctlm  24022  ressust  24089  uspreg  24100  ucncn  24111  neipcfilu  24122  cuspusp  24126  metxmet  24161  xmstps  24280  msxms  24281  xmsxmet  24283  msmet  24284  nrgngp  24500  nlmngp  24515  nlmlmod  24516  nlmnrg  24517  nvcnlm  24534  nmoi  24566  nghmrcl1  24570  nghmrcl2  24571  nmhmrcl1  24585  nmhmrcl2  24586  qdensere  24607  xrge0gsumle  24670  xrge0tsms  24671  icopnfcnv  24788  cvsclm  24974  cphsscph  25100  cmetmet  25135  cmsms  25197  hlbn  25212  ovolicc2lem5  25371  mblss  25381  mbff  25475  mbfres  25494  i1fmbf  25525  limcmpt  25733  c1liplem1  25850  c1lip2  25852  fta1glem1  26022  fta1glem2  26023  fta1g  26024  fta1b  26026  ply1pid  26036  aacn  26170  ulmf2  26236  logdmnrp  26490  logdmss  26491  logcnlem2  26492  logcnlem3  26493  logcnlem4  26494  logcnlem5  26495  logcn  26496  dvloglem  26497  logf1o2  26499  efopnlem1  26505  logtayl2  26511  cxpcn  26594  cxpcnOLD  26595  cxpcn3lem  26597  cxpcn3  26598  resqrtcn  26599  atandmneg  26753  atandmcj  26756  cosatan  26768  cosatanne0  26769  birthdaylem1  26798  areacl  26809  cxp2lim  26824  jensenlem2  26835  jensen  26836  sqff1o  27029  mpodvdsmulf1o  27041  dvdsmulf1o  27043  lgsqrlem1  27194  lgsqrlem2  27195  lgsqrlem3  27196  lgsqrlem4  27197  lgseisenlem3  27225  chebbnd1  27320  chtppilim  27323  chpchtlim  27327  chpo1ub  27328  dchrmusumlema  27341  dchrvmasumiflem1  27349  dchrisum0lema  27362  dchrisum0lem2  27366  selberg3lem2  27406  pntrsumo1  27413  selbergsb  27423  pnt2  27461  sltres  27510  noseponlem  27512  tglineeltr  28317  axcontlem2  28658  axcontlem7  28663  axcontlem8  28664  uhgr0vb  28767  lfuhgr1v0e  28946  fusgrusgr  29014  uvtxisvtx  29081  nbupgruvtxres  29099  cusgrusgr  29111  trliswlk  29389  clwlkiswlk  29466  clwwlkclwwlkn  29718  eupthistrl  29899  frgrusgr  29949  frgrwopreglem5  30009  clwwnonrepclwwnon  30033  ablogrpo  30235  bnnv  30554  hlobn  30576  hcauseq  30873  hlimseqi  30877  hlimveci  30878  shss  30898  sh0  30904  chsh  30912  lnopf  31547  bdopln  31549  hmopf  31562  lnfnf  31572  unopf1o  31604  elunop2  31701  elpjhmop  31873  stcltrlem1  31964  mdslle1i  32005  mdslle2i  32006  2reu2rex1  32156  2reureurex  32157  ssnnssfz  32433  xrge0tsmsd  32643  ogrpgrp  32655  isdrng4  32827  ofldfld  32860  ofldlt1  32863  ofldchr  32864  isarchiofld  32867  reofld  32891  rearchi  32893  quslsm  32951  srafldlvec  33118  rgmoddimOLD  33140  extdggt0  33181  fldextid  33183  extdgid  33184  extdgmul  33185  extdg1id  33187  ist0cld  33268  creftop  33281  lmxrge0  33387  qqhrhm  33424  esumpcvgval  33531  dynkin  33620  measssd  33668  elmbfmvol2  33721  omssubadd  33754  sibfinima  33793  eulerpartlemr  33828  eulerpartlemgf  33833  fiblem  33852  domprobmeas  33864  ballotlemscr  33972  ballotlemfg  33979  ballotlemfrc  33980  ballotlemfrceq  33982  ballotlemrinv0  33986  chtvalz  34096  bnj563  34209  bnj658  34217  bnj667  34218  bnj570  34371  bnj938  34403  bnj1001  34425  bnj1006  34426  bnj1049  34440  bnj1121  34451  bnj1173  34468  bnj1177  34472  bnj1245  34480  bnj1311  34490  bnj1321  34493  bnj1388  34499  bnj1398  34500  bnj1415  34504  bnj1417  34507  bnj1421  34508  bnj1442  34515  bnj1452  34518  bnj1489  34522  bnj1312  34524  pthacycspth  34603  pconntop  34671  sconnpconn  34673  cvmcn  34708  cvmliftlem10  34740  sate0fv0  34863  fundmpss  35199  txpss3v  35311  pprodss4v  35317  outsideofcol  35566  fnebas  35685  filnetlem3  35721  bj-nnfe  36065  bj-xpcossxp  36526  bj-rvecmod  36632  pibt2  36754  phpreu  36928  matunitlindflem1  36940  matunitlindflem2  36941  matunitlindf  36942  poimirlem26  36970  itg2addnc  36998  istotbnd3  37095  totbndmet  37096  sstotbnd2  37098  sstotbnd  37099  equivtotbnd  37102  bndmet  37105  totbndbnd  37113  prdstotbnd  37118  smgrpismgmOLD  37186  mndoissmgrpOLD  37192  crngorngo  37324  prrngorngo  37375  divrngpr  37377  xrnss3v  37698  dfxrn2  37702  refressn  37769  antisymressn  37770  symrelim  37885  eqvrelsym  37931  eqvreltr  37933  disjorimxrn  38074  disjim  38107  disjlem14  38124  ollat  38539  omlol  38566  cvlatl  38651  hlomcmcv  38682  2dim  38797  1dimN  38798  lcfl8b  40831  lclkrlem2  40859  lclkrslem1  40864  lclkrslem2  40865  lcfrlem9  40877  mapdval2N  40957  mapdordlem2  40964  mapdrvallem2  40972  nacsacs  41902  eldiophelnn0  41957  lnmlmod  42276  lnrring  42309  mncply  42334  idomrootle  42392  idomodle  42393  areaquad  42420  dfno2  42634  harval3  42744  alephiso3  42765  mnurndlem1  43495  nznngen  43530  binomcxplemcvg  43568  2uasbanh  43777  disjinfi  44342  climxrre  44917  mbfdmssre  45167  stoweidlem14  45181  stoweidlem16  45183  stoweidlem24  45191  stoweidlem51  45218  stoweidlem54  45221  etransclem32  45433  sge0fodjrnlem  45583  pimrecltpos  45875  pimrecltneg  45891  smfaddlem1  45930  smflimsuplem7  45993  upwordisword  46046  ndmafv  46299  dfafv23  46412  dfatcolem  46414  dfatco  46415  evenz  46749  oddz  46750  gbeeven  46873  gbowodd  46874  ssnn0ssfz  47180  elbigof  47394  digvalnn0  47439  2sphere  47589  mof0  47658  mof0ALT  47660  thincc  47798