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  2570  reurex  3358  rabidim1  3428  pssss  4061  eldifi  4094  elinel1  4164  ssunsn2  4791  pwssun  5530  sopo  5565  wefr  5628  opelxp1  5680  relop  5814  ssrelrn  5858  ordtr  6346  funmo  6531  funmoOLD  6532  funrel  6533  fnfun  6618  ffn  6688  f1f  6756  f1of1  6799  f1ofo  6807  isof1o  7298  eqopi  8004  1st2nd2  8007  reldmtpos  8213  brinxper  8700  swoer  8702  ecopover  8794  sdomdom  8951  mapfien  9359  inf3lemd  9580  cardprclem  9932  infxpenlem  9966  cardinfima  10050  dfac5lem4  10079  dfac5lem4OLD  10081  domtriomlem  10395  smobeth  10539  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  axrnegex  11115  axpre-sup  11122  zre  12533  ixxss1  13324  ixxss2  13325  ixxss12  13326  lbioo  13337  ubioo  13338  iccss2  13378  rge0ssre  13417  elfzuz  13481  0wrd0  14505  01sqrexlem6  15213  rlimf  15467  lo1f  15484  lo1dm  15485  o1f  15495  o1dm  15496  mertenslem2  15851  divalglem9  16371  bitsinv2  16413  bitsf1ocnv  16414  gcdcllem1  16469  coprmproddvdslem  16632  prmnn  16644  prmuz2  16666  phimullem  16749  hashgcdlem  16758  1arith  16898  ramtlecl  16971  0ramcl  16994  firest  17395  acsmre  17613  posprs  18277  tospos  18379  latpos  18397  clatpos  18460  dlatl  18483  pslem  18531  tsrlemax  18545  tsrps  18546  sgrpmgm  18651  mndsgrp  18667  grpmnd  18872  nsgsubg  19090  ghmgrp1  19150  ghmgrp2  19151  gimghm  19196  gagrp  19224  gaset  19225  psgneu  19436  efgredeu  19682  ablgrp  19715  cmnmnd  19727  cyggenod2  19815  cyggrp  19820  dprd2dlem1  19973  dprd2da  19974  ablfac2  20021  simpggrp  20026  crngring  20154  dvdsrcl  20274  unitcl  20284  rimrhmOLD  20404  rimrhm  20405  brric2  20415  nzrringOLD  20426  subrgring  20483  subrgrcl  20485  rnghmsubcsetclem1  20540  funcrngcsetcALT  20550  rhmsubcsetclem1  20569  rhmsubcrngclem1  20575  domnnzr  20615  drngring  20645  flddrngd  20650  rng1nfld  20688  srngrhm  20754  lmimlmhm  20971  lveclmod  21013  2idlelbas  21174  rng2idlsubgsubrng  21178  2idlcpblrng  21181  2idlcpbl  21182  qus1  21184  qusrhm  21186  lpirring  21241  cygznlem1  21476  cygznlem3  21479  lbslinds  21742  assalmod  21769  assaring  21770  gsummatr01lem1  22542  topontop  22800  tpstop  22824  mretopd  22979  neiptoptop  23018  perftop  23043  restfpw  23066  cntop1  23127  cntop2  23128  cnptop1  23129  cnptop2  23130  cnprcl  23132  t1ficld  23214  t0top  23216  t1top  23217  haustop  23218  regtop  23220  nrmtop  23223  cnrmtop  23224  pnrmnrm  23227  cmptop  23282  tgcmp  23288  conndisj  23303  conntop  23304  1stctop  23330  llytop  23359  nllytop  23360  hmeocn  23647  filfbas  23735  ufilfil  23791  flimtop  23852  flimfil  23856  alexsublem  23931  ptcmplem3  23941  tsmsfbas  24015  tsmslem1  24016  tsmsgsum  24026  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  tsmsmhm  24033  tsmsadd  24034  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  tlmtmd  24074  tlmlmod  24076  tlmtrg  24077  tvctlm  24084  ressust  24151  uspreg  24161  ucncn  24172  neipcfilu  24183  cuspusp  24187  metxmet  24222  xmstps  24341  msxms  24342  xmsxmet  24344  msmet  24345  nrgngp  24550  nlmngp  24565  nlmlmod  24566  nlmnrg  24567  nvcnlm  24584  nmoi  24616  nghmrcl1  24620  nghmrcl2  24621  nmhmrcl1  24635  nmhmrcl2  24636  qdensere  24657  xrge0gsumle  24722  xrge0tsms  24723  icopnfcnv  24840  cvsclm  25026  cphsscph  25151  cmetmet  25186  cmsms  25248  hlbn  25263  ovolicc2lem5  25422  mblss  25432  mbff  25526  mbfres  25545  i1fmbf  25576  limcmpt  25784  c1liplem1  25901  c1lip2  25903  fta1glem1  26073  fta1glem2  26074  fta1g  26075  fta1b  26077  idomrootle  26078  ply1pid  26088  aacn  26225  ulmf2  26293  logdmnrp  26550  logdmss  26551  logcnlem2  26552  logcnlem3  26553  logcnlem4  26554  logcnlem5  26555  logcn  26556  dvloglem  26557  logf1o2  26559  efopnlem1  26565  logtayl2  26571  cxpcn  26654  cxpcnOLD  26655  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  atandmneg  26816  atandmcj  26819  cosatan  26831  cosatanne0  26832  birthdaylem1  26861  areacl  26872  cxp2lim  26887  jensenlem2  26898  jensen  26899  sqff1o  27092  mpodvdsmulf1o  27104  dvdsmulf1o  27106  lgsqrlem1  27257  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  lgseisenlem3  27288  chebbnd1  27383  chtppilim  27386  chpchtlim  27390  chpo1ub  27391  dchrmusumlema  27404  dchrvmasumiflem1  27412  dchrisum0lema  27425  dchrisum0lem2  27429  selberg3lem2  27469  pntrsumo1  27476  selbergsb  27486  pnt2  27524  sltres  27574  noseponlem  27576  tglineeltr  28558  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  uhgr0vb  28999  lfuhgr1v0e  29181  fusgrusgr  29249  uvtxisvtx  29316  nbupgruvtxres  29334  cusgrusgr  29346  trliswlk  29625  clwlkiswlk  29704  clwwlkclwwlkn  29959  eupthistrl  30140  frgrusgr  30190  frgrwopreglem5  30250  clwwnonrepclwwnon  30274  ablogrpo  30476  bnnv  30795  hlobn  30817  hcauseq  31114  hlimseqi  31118  hlimveci  31119  shss  31139  sh0  31145  chsh  31153  lnopf  31788  bdopln  31790  hmopf  31803  lnfnf  31813  unopf1o  31845  elunop2  31942  elpjhmop  32114  stcltrlem1  32205  mdslle1i  32246  mdslle2i  32247  2reu2rex1  32410  2reureurex  32411  ssnnssfz  32710  chnwrd  32933  xrge0tsmsd  33002  ogrpgrp  33017  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  isdrng4  33245  ofldfld  33288  ofldlt1  33291  ofldchr  33292  isarchiofld  33295  reofld  33315  rearchi  33317  quslsm  33376  ufdidom  33513  srafldlvec  33582  rgmoddimOLD  33606  extdggt0  33653  fldextid  33655  extdgid  33656  extdgmul  33659  extdg1id  33661  ist0cld  33823  creftop  33836  lmxrge0  33942  qqhrhm  33979  esumpcvgval  34068  dynkin  34157  measssd  34205  elmbfmvol2  34258  omssubadd  34291  sibfinima  34330  eulerpartlemr  34365  eulerpartlemgf  34370  fiblem  34389  domprobmeas  34401  ballotlemscr  34510  ballotlemfg  34517  ballotlemfrc  34518  ballotlemfrceq  34520  ballotlemrinv0  34524  chtvalz  34620  bnj563  34733  bnj658  34741  bnj667  34742  bnj570  34895  bnj938  34927  bnj1001  34949  bnj1006  34950  bnj1049  34964  bnj1121  34975  bnj1173  34992  bnj1177  34996  bnj1245  35004  bnj1311  35014  bnj1321  35017  bnj1388  35023  bnj1398  35024  bnj1415  35028  bnj1417  35031  bnj1421  35032  bnj1442  35039  bnj1452  35042  bnj1489  35046  bnj1312  35048  pthacycspth  35144  pconntop  35212  sconnpconn  35214  cvmcn  35249  cvmliftlem10  35281  sate0fv0  35404  fundmpss  35754  txpss3v  35866  pprodss4v  35872  outsideofcol  36121  fnebas  36332  filnetlem3  36368  bj-nnfe  36719  bj-xpcossxp  37177  bj-rvecmod  37283  pibt2  37405  phpreu  37598  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  poimirlem26  37640  itg2addnc  37668  istotbnd3  37765  totbndmet  37766  sstotbnd2  37768  sstotbnd  37769  equivtotbnd  37772  bndmet  37775  totbndbnd  37783  prdstotbnd  37788  smgrpismgmOLD  37856  mndoissmgrpOLD  37862  crngorngo  37994  prrngorngo  38045  divrngpr  38047  xrnss3v  38354  dfxrn2  38358  refressn  38434  antisymressn  38435  symrelim  38550  eqvrelsym  38596  eqvreltr  38598  disjorimxrn  38740  disjim  38773  disjlem14  38790  ollat  39206  omlol  39233  cvlatl  39318  hlomcmcv  39349  2dim  39464  1dimN  39465  lcfl8b  41498  lclkrlem2  41526  lclkrslem1  41531  lclkrslem2  41532  lcfrlem9  41544  mapdval2N  41624  mapdordlem2  41631  mapdrvallem2  41639  idomnnzgmulnz  42121  aks6d1c6lem3  42160  readvrec2  42349  readvrec  42350  readvcot  42352  nacsacs  42697  eldiophelnn0  42752  lnmlmod  43068  lnrring  43101  mncply  43126  idomodle  43180  areaquad  43205  dfno2  43417  harval3  43527  alephiso3  43548  mnurndlem1  44270  nznngen  44305  binomcxplemcvg  44343  2uasbanh  44551  relpf  44940  disjinfi  45186  climxrre  45748  mbfdmssre  45998  stoweidlem14  46012  stoweidlem16  46014  stoweidlem24  46022  stoweidlem51  46049  stoweidlem54  46052  etransclem32  46264  sge0fodjrnlem  46414  pimrecltpos  46706  pimrecltneg  46722  smfaddlem1  46761  smflimsuplem7  46824  upwordisword  46879  ndmafv  47141  dfafv23  47254  dfatcolem  47256  dfatco  47257  evenz  47631  oddz  47632  gbeeven  47755  gbowodd  47756  sclnbgrisvtx  47849  ssnn0ssfz  48337  elbigof  48543  digvalnn0  48588  2sphere  48738  mof0  48826  mof0ALT  48828  uobeq2  49390  thincc  49411  termcthin  49466