Theorem simplbi 496

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  660  xoror  1520  euex  2577  reurex  3346  rabidim1  3411  pssss  4038  eldifi  4071  elinel1  4141  ssunsn2  4770  pwssun  5523  sopo  5558  wefr  5621  opelxp1  5673  relop  5805  ssrelrn  5849  ordtr  6337  funmo  6514  funrel  6515  fnfun  6598  ffn  6668  f1f  6736  f1of1  6779  f1ofo  6787  isof1o  7278  eqopi  7978  1st2nd2  7981  reldmtpos  8184  brinxper  8673  swoer  8675  ecopover  8768  sdomdom  8927  mapfien  9321  inf3lemd  9548  cardprclem  9903  infxpenlem  9935  cardinfima  10019  dfac5lem4  10048  dfac5lem4OLD  10050  domtriomlem  10364  smobeth  10509  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  axrnegex  11085  axpre-sup  11092  zre  12528  ixxss1  13316  ixxss2  13317  ixxss12  13318  lbioo  13329  ubioo  13330  iccss2  13370  rge0ssre  13409  elfzuz  13474  0wrd0  14502  01sqrexlem6  15209  rlimf  15463  lo1f  15480  lo1dm  15481  o1f  15491  o1dm  15492  mertenslem2  15850  divalglem9  16370  bitsinv2  16412  bitsf1ocnv  16413  gcdcllem1  16468  coprmproddvdslem  16631  prmnn  16643  prmuz2  16665  phimullem  16749  hashgcdlem  16758  1arith  16898  ramtlecl  16971  0ramcl  16994  firest  17395  acsmre  17618  posprs  18282  tospos  18384  latpos  18404  clatpos  18467  dlatl  18490  pslem  18538  tsrlemax  18552  tsrps  18553  chnwrd  18574  sgrpmgm  18692  mndsgrp  18708  grpmnd  18916  nsgsubg  19133  ghmgrp1  19193  ghmgrp2  19194  gimghm  19239  gagrp  19267  gaset  19268  psgneu  19481  efgredeu  19727  ablgrp  19760  cmnmnd  19772  cyggenod2  19860  cyggrp  19865  dprd2dlem1  20018  dprd2da  20019  ablfac2  20066  simpggrp  20071  ogrpgrp  20100  crngring  20226  dvdsrcl  20345  unitcl  20355  rimrhm  20473  brric2  20483  nzrringOLD  20494  subrgring  20551  subrgrcl  20553  rnghmsubcsetclem1  20608  funcrngcsetcALT  20618  rhmsubcsetclem1  20637  rhmsubcrngclem1  20643  domnnzr  20683  drngring  20713  flddrngd  20718  rng1nfld  20756  srngrhm  20822  ofldfld  20849  ofldlt1  20852  lmimlmhm  21059  lveclmod  21101  2idlelbas  21262  rng2idlsubgsubrng  21266  2idlcpblrng  21269  2idlcpbl  21270  qus1  21272  qusrhm  21274  lpirring  21329  cygznlem1  21546  cygznlem3  21549  ofldchr  21556  lbslinds  21813  assalmod  21840  assaring  21841  gsummatr01lem1  22620  topontop  22878  tpstop  22902  mretopd  23057  neiptoptop  23096  perftop  23121  restfpw  23144  cntop1  23205  cntop2  23206  cnptop1  23207  cnptop2  23208  cnprcl  23210  t1ficld  23292  t0top  23294  t1top  23295  haustop  23296  regtop  23298  nrmtop  23301  cnrmtop  23302  pnrmnrm  23305  cmptop  23360  tgcmp  23366  conndisj  23381  conntop  23382  1stctop  23408  llytop  23437  nllytop  23438  hmeocn  23725  filfbas  23813  ufilfil  23869  flimtop  23930  flimfil  23934  alexsublem  24009  ptcmplem3  24019  tsmsfbas  24093  tsmslem1  24094  tsmsgsum  24104  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  tsmsmhm  24111  tsmsadd  24112  tsmsxplem1  24118  tsmsxplem2  24119  tsmsxp  24120  tlmtmd  24152  tlmlmod  24154  tlmtrg  24155  tvctlm  24162  ressust  24228  uspreg  24238  ucncn  24249  neipcfilu  24260  cuspusp  24264  metxmet  24299  xmstps  24418  msxms  24419  xmsxmet  24421  msmet  24422  nrgngp  24627  nlmngp  24642  nlmlmod  24643  nlmnrg  24644  nvcnlm  24661  nmoi  24693  nghmrcl1  24697  nghmrcl2  24698  nmhmrcl1  24712  nmhmrcl2  24713  qdensere  24734  xrge0gsumle  24799  xrge0tsms  24800  icopnfcnv  24909  cvsclm  25093  cphsscph  25218  cmetmet  25253  cmsms  25315  hlbn  25330  ovolicc2lem5  25488  mblss  25498  mbff  25592  mbfres  25611  i1fmbf  25642  limcmpt  25850  c1liplem1  25963  c1lip2  25965  fta1glem1  26133  fta1glem2  26134  fta1g  26135  fta1b  26137  idomrootle  26138  ply1pid  26148  aacn  26283  ulmf2  26349  logdmnrp  26605  logdmss  26606  logcnlem2  26607  logcnlem3  26608  logcnlem4  26609  logcnlem5  26610  logcn  26611  dvloglem  26612  logf1o2  26614  efopnlem1  26620  logtayl2  26626  cxpcn  26709  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  atandmneg  26870  atandmcj  26873  cosatan  26885  cosatanne0  26886  birthdaylem1  26915  areacl  26926  cxp2lim  26940  jensenlem2  26951  jensen  26952  sqff1o  27145  mpodvdsmulf1o  27157  dvdsmulf1o  27159  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  lgseisenlem3  27340  chebbnd1  27435  chtppilim  27438  chpchtlim  27442  chpo1ub  27443  dchrmusumlema  27456  dchrvmasumiflem1  27464  dchrisum0lema  27477  dchrisum0lem2  27481  selberg3lem2  27521  pntrsumo1  27528  selbergsb  27538  pnt2  27576  ltsres  27626  noseponlem  27628  reno  28484  tglineeltr  28699  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  uhgr0vb  29141  lfuhgr1v0e  29323  fusgrusgr  29391  uvtxisvtx  29458  nbupgruvtxres  29476  cusgrusgr  29488  trliswlk  29764  clwlkiswlk  29842  clwwlkclwwlkn  30100  eupthistrl  30281  frgrusgr  30331  frgrwopreglem5  30391  clwwnonrepclwwnon  30415  ablogrpo  30618  bnnv  30937  hlobn  30959  hcauseq  31256  hlimseqi  31260  hlimveci  31261  shss  31281  sh0  31287  chsh  31295  lnopf  31930  bdopln  31932  hmopf  31945  lnfnf  31955  unopf1o  31987  elunop2  32084  elpjhmop  32256  stcltrlem1  32347  mdslle1i  32388  mdslle2i  32389  2reu2rex1  32550  2reureurex  32551  ssnnssfz  32860  xrge0tsmsd  33134  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  isdrng4  33356  reofld  33403  rearchi  33406  quslsm  33465  ufdidom  33602  mplvrpmga  33689  srafldlvec  33730  extdggt0  33801  fldextid  33803  extdgid  33804  extdgmul  33807  extdg1id  33810  ist0cld  33977  creftop  33990  lmxrge0  34096  qqhrhm  34133  esumpcvgval  34222  dynkin  34311  measssd  34359  elmbfmvol2  34411  omssubadd  34444  sibfinima  34483  eulerpartlemr  34518  eulerpartlemgf  34523  fiblem  34542  domprobmeas  34554  ballotlemscr  34663  ballotlemfg  34670  ballotlemfrc  34671  ballotlemfrceq  34673  ballotlemrinv0  34677  chtvalz  34773  bnj563  34886  bnj658  34894  bnj667  34895  bnj570  35047  bnj938  35079  bnj1001  35101  bnj1006  35102  bnj1049  35116  bnj1121  35127  bnj1173  35144  bnj1177  35148  bnj1245  35156  bnj1311  35166  bnj1321  35169  bnj1388  35175  bnj1398  35176  bnj1415  35180  bnj1417  35183  bnj1421  35184  bnj1442  35191  bnj1452  35194  bnj1489  35198  bnj1312  35200  pthacycspth  35339  pconntop  35407  sconnpconn  35409  cvmcn  35444  cvmliftlem10  35476  sate0fv0  35599  fundmpss  35949  txpss3v  36058  pprodss4v  36064  outsideofcol  36315  fnebas  36526  filnetlem3  36562  bj-nnfe  37028  bj-xpcossxp  37503  bj-rvecmod  37609  pibt2  37733  phpreu  37925  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  poimirlem26  37967  itg2addnc  37995  istotbnd3  38092  totbndmet  38093  sstotbnd2  38095  sstotbnd  38096  equivtotbnd  38099  bndmet  38102  totbndbnd  38110  prdstotbnd  38115  smgrpismgmOLD  38183  mndoissmgrpOLD  38189  crngorngo  38321  prrngorngo  38372  divrngpr  38374  xrnss3v  38702  dfxrn2  38706  refressn  38854  antisymressn  38855  symrelim  38964  eqvrelsym  39010  eqvreltr  39012  disjimeceqim  39125  disjorimxrn  39169  disjim  39205  disjlem14  39222  ollat  39659  omlol  39686  cvlatl  39771  hlomcmcv  39802  2dim  39916  1dimN  39917  lcfl8b  41950  lclkrlem2  41978  lclkrslem1  41983  lclkrslem2  41984  lcfrlem9  41996  mapdval2N  42076  mapdordlem2  42083  mapdrvallem2  42091  idomnnzgmulnz  42572  aks6d1c6lem3  42611  readvrec2  42793  readvrec  42794  readvcot  42796  nacsacs  43141  eldiophelnn0  43196  lnmlmod  43507  lnrring  43540  mncply  43565  idomodle  43619  areaquad  43644  dfno2  43855  harval3  43965  alephiso3  43986  mnurndlem1  44708  nznngen  44743  binomcxplemcvg  44781  2uasbanh  44988  relpf  45377  disjinfi  45622  climxrre  46178  mbfdmssre  46428  stoweidlem14  46442  stoweidlem16  46444  stoweidlem24  46452  stoweidlem51  46479  stoweidlem54  46482  etransclem32  46694  sge0fodjrnlem  46844  pimrecltpos  47136  pimrecltneg  47152  smfaddlem1  47191  smflimsuplem7  47254  ndmafv  47588  dfafv23  47701  dfatcolem  47703  dfatco  47704  evenz  48106  oddz  48107  gbeeven  48230  gbowodd  48231  sclnbgrisvtx  48325  grlimgredgex  48476  ssnn0ssfz  48825  elbigof  49030  digvalnn0  49075  2sphere  49225  mof0  49313  mof0ALT  49315  uobeq2  49876  thincc  49897  termcthin  49952