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  658  xoror  1515  euex  2580  reurex  3392  rabidim1  3466  pssss  4121  eldifi  4154  elinel1  4224  ssunsn2  4852  pwssun  5590  sopo  5627  wefr  5690  opelxp1  5742  relop  5875  ssrelrn  5919  ordtr  6409  funmo  6593  funmoOLD  6594  funrel  6595  fnfun  6679  ffn  6747  f1f  6817  f1of1  6861  f1ofo  6869  isof1o  7359  eqopi  8066  1st2nd2  8069  reldmtpos  8275  brinxper  8792  swoer  8794  ecopover  8879  sdomdom  9040  mapfien  9477  inf3lemd  9696  cardprclem  10048  infxpenlem  10082  cardinfima  10166  dfac5lem4  10195  dfac5lem4OLD  10197  domtriomlem  10511  smobeth  10655  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  axrnegex  11231  axpre-sup  11238  zre  12643  ixxss1  13425  ixxss2  13426  ixxss12  13427  lbioo  13438  ubioo  13439  iccss2  13478  rge0ssre  13516  elfzuz  13580  0wrd0  14588  01sqrexlem6  15296  rlimf  15547  lo1f  15564  lo1dm  15565  o1f  15575  o1dm  15576  mertenslem2  15933  divalglem9  16449  bitsinv2  16489  bitsf1ocnv  16490  gcdcllem1  16545  coprmproddvdslem  16709  prmnn  16721  prmuz2  16743  phimullem  16826  hashgcdlem  16835  1arith  16974  ramtlecl  17047  0ramcl  17070  firest  17492  acsmre  17710  posprs  18386  tospos  18490  latpos  18508  clatpos  18571  dlatl  18594  pslem  18642  tsrlemax  18656  tsrps  18657  sgrpmgm  18762  mndsgrp  18778  grpmnd  18980  nsgsubg  19198  ghmgrp1  19258  ghmgrp2  19259  gimghm  19304  gagrp  19332  gaset  19333  psgneu  19548  efgredeu  19794  ablgrp  19827  cmnmnd  19839  cyggenod2  19927  cyggrp  19932  dprd2dlem1  20085  dprd2da  20086  ablfac2  20133  simpggrp  20138  crngring  20272  dvdsrcl  20391  unitcl  20401  rimrhmOLD  20521  rimrhm  20522  brric2  20532  nzrringOLD  20543  subrgring  20602  subrgrcl  20604  rnghmsubcsetclem1  20653  funcrngcsetcALT  20663  rhmsubcsetclem1  20682  rhmsubcrngclem1  20688  domnnzr  20728  drngring  20758  flddrngd  20763  fldidomOLD  20794  rng1nfld  20802  srngrhm  20868  lmimlmhm  21086  lveclmod  21128  2idlelbas  21297  rng2idlsubgsubrng  21301  2idlcpblrng  21304  2idlcpbl  21305  qus1  21307  qusrhm  21309  lpirring  21364  cygznlem1  21608  cygznlem3  21611  lbslinds  21876  assalmod  21903  assaring  21904  gsummatr01lem1  22682  topontop  22940  tpstop  22964  mretopd  23121  neiptoptop  23160  perftop  23185  restfpw  23208  cntop1  23269  cntop2  23270  cnptop1  23271  cnptop2  23272  cnprcl  23274  t1ficld  23356  t0top  23358  t1top  23359  haustop  23360  regtop  23362  nrmtop  23365  cnrmtop  23366  pnrmnrm  23369  cmptop  23424  tgcmp  23430  conndisj  23445  conntop  23446  1stctop  23472  llytop  23501  nllytop  23502  hmeocn  23789  filfbas  23877  ufilfil  23933  flimtop  23994  flimfil  23998  alexsublem  24073  ptcmplem3  24083  tsmsfbas  24157  tsmslem1  24158  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  tsmsmhm  24175  tsmsadd  24176  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  tlmtmd  24216  tlmlmod  24218  tlmtrg  24219  tvctlm  24226  ressust  24293  uspreg  24304  ucncn  24315  neipcfilu  24326  cuspusp  24330  metxmet  24365  xmstps  24484  msxms  24485  xmsxmet  24487  msmet  24488  nrgngp  24704  nlmngp  24719  nlmlmod  24720  nlmnrg  24721  nvcnlm  24738  nmoi  24770  nghmrcl1  24774  nghmrcl2  24775  nmhmrcl1  24789  nmhmrcl2  24790  qdensere  24811  xrge0gsumle  24874  xrge0tsms  24875  icopnfcnv  24992  cvsclm  25178  cphsscph  25304  cmetmet  25339  cmsms  25401  hlbn  25416  ovolicc2lem5  25575  mblss  25585  mbff  25679  mbfres  25698  i1fmbf  25729  limcmpt  25938  c1liplem1  26055  c1lip2  26057  fta1glem1  26227  fta1glem2  26228  fta1g  26229  fta1b  26231  idomrootle  26232  ply1pid  26242  aacn  26377  ulmf2  26445  logdmnrp  26701  logdmss  26702  logcnlem2  26703  logcnlem3  26704  logcnlem4  26705  logcnlem5  26706  logcn  26707  dvloglem  26708  logf1o2  26710  efopnlem1  26716  logtayl2  26722  cxpcn  26805  cxpcnOLD  26806  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  atandmneg  26967  atandmcj  26970  cosatan  26982  cosatanne0  26983  birthdaylem1  27012  areacl  27023  cxp2lim  27038  jensenlem2  27049  jensen  27050  sqff1o  27243  mpodvdsmulf1o  27255  dvdsmulf1o  27257  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  lgseisenlem3  27439  chebbnd1  27534  chtppilim  27537  chpchtlim  27541  chpo1ub  27542  dchrmusumlema  27555  dchrvmasumiflem1  27563  dchrisum0lema  27576  dchrisum0lem2  27580  selberg3lem2  27620  pntrsumo1  27627  selbergsb  27637  pnt2  27675  sltres  27725  noseponlem  27727  tglineeltr  28657  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  uhgr0vb  29107  lfuhgr1v0e  29289  fusgrusgr  29357  uvtxisvtx  29424  nbupgruvtxres  29442  cusgrusgr  29454  trliswlk  29733  clwlkiswlk  29810  clwwlkclwwlkn  30062  eupthistrl  30243  frgrusgr  30293  frgrwopreglem5  30353  clwwnonrepclwwnon  30377  ablogrpo  30579  bnnv  30898  hlobn  30920  hcauseq  31217  hlimseqi  31221  hlimveci  31222  shss  31242  sh0  31248  chsh  31256  lnopf  31891  bdopln  31893  hmopf  31906  lnfnf  31916  unopf1o  31948  elunop2  32045  elpjhmop  32217  stcltrlem1  32308  mdslle1i  32349  mdslle2i  32350  2reu2rex1  32509  2reureurex  32510  ssnnssfz  32792  chnwrd  32980  xrge0tsmsd  33041  ogrpgrp  33053  isdrng4  33264  ofldfld  33305  ofldlt1  33308  ofldchr  33309  isarchiofld  33312  reofld  33337  rearchi  33339  quslsm  33398  ufdidom  33535  srafldlvec  33601  rgmoddimOLD  33623  extdggt0  33670  fldextid  33672  extdgid  33673  extdgmul  33674  extdg1id  33676  ist0cld  33779  creftop  33792  lmxrge0  33898  qqhrhm  33935  esumpcvgval  34042  dynkin  34131  measssd  34179  elmbfmvol2  34232  omssubadd  34265  sibfinima  34304  eulerpartlemr  34339  eulerpartlemgf  34344  fiblem  34363  domprobmeas  34375  ballotlemscr  34483  ballotlemfg  34490  ballotlemfrc  34491  ballotlemfrceq  34493  ballotlemrinv0  34497  chtvalz  34606  bnj563  34719  bnj658  34727  bnj667  34728  bnj570  34881  bnj938  34913  bnj1001  34935  bnj1006  34936  bnj1049  34950  bnj1121  34961  bnj1173  34978  bnj1177  34982  bnj1245  34990  bnj1311  35000  bnj1321  35003  bnj1388  35009  bnj1398  35010  bnj1415  35014  bnj1417  35017  bnj1421  35018  bnj1442  35025  bnj1452  35028  bnj1489  35032  bnj1312  35034  pthacycspth  35125  pconntop  35193  sconnpconn  35195  cvmcn  35230  cvmliftlem10  35262  sate0fv0  35385  fundmpss  35730  txpss3v  35842  pprodss4v  35848  outsideofcol  36097  fnebas  36310  filnetlem3  36346  bj-nnfe  36697  bj-xpcossxp  37155  bj-rvecmod  37261  pibt2  37383  phpreu  37564  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  poimirlem26  37606  itg2addnc  37634  istotbnd3  37731  totbndmet  37732  sstotbnd2  37734  sstotbnd  37735  equivtotbnd  37738  bndmet  37741  totbndbnd  37749  prdstotbnd  37754  smgrpismgmOLD  37822  mndoissmgrpOLD  37828  crngorngo  37960  prrngorngo  38011  divrngpr  38013  xrnss3v  38328  dfxrn2  38332  refressn  38399  antisymressn  38400  symrelim  38515  eqvrelsym  38561  eqvreltr  38563  disjorimxrn  38704  disjim  38737  disjlem14  38754  ollat  39169  omlol  39196  cvlatl  39281  hlomcmcv  39312  2dim  39427  1dimN  39428  lcfl8b  41461  lclkrlem2  41489  lclkrslem1  41494  lclkrslem2  41495  lcfrlem9  41507  mapdval2N  41587  mapdordlem2  41594  mapdrvallem2  41602  idomnnzgmulnz  42090  aks6d1c6lem3  42129  nacsacs  42665  eldiophelnn0  42720  lnmlmod  43036  lnrring  43069  mncply  43094  idomodle  43152  areaquad  43177  dfno2  43390  harval3  43500  alephiso3  43521  mnurndlem1  44250  nznngen  44285  binomcxplemcvg  44323  2uasbanh  44532  disjinfi  45099  climxrre  45671  mbfdmssre  45921  stoweidlem14  45935  stoweidlem16  45937  stoweidlem24  45945  stoweidlem51  45972  stoweidlem54  45975  etransclem32  46187  sge0fodjrnlem  46337  pimrecltpos  46629  pimrecltneg  46645  smfaddlem1  46684  smflimsuplem7  46747  upwordisword  46800  ndmafv  47055  dfafv23  47168  dfatcolem  47170  dfatco  47171  evenz  47504  oddz  47505  gbeeven  47628  gbowodd  47629  sclnbgrisvtx  47721  ssnn0ssfz  48074  elbigof  48288  digvalnn0  48333  2sphere  48483  mof0  48551  mof0ALT  48553  thincc  48691