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  1519  euex  2574  reurex  3351  rabidim1  3418  pssss  4047  eldifi  4080  elinel1  4150  ssunsn2  4778  pwssun  5511  sopo  5546  wefr  5609  opelxp1  5661  relop  5794  ssrelrn  5838  ordtr  6325  funmo  6502  funrel  6503  fnfun  6586  ffn  6656  f1f  6724  f1of1  6767  f1ofo  6775  isof1o  7263  eqopi  7963  1st2nd2  7966  reldmtpos  8170  brinxper  8657  swoer  8659  ecopover  8751  sdomdom  8909  mapfien  9299  inf3lemd  9524  cardprclem  9879  infxpenlem  9911  cardinfima  9995  dfac5lem4  10024  dfac5lem4OLD  10026  domtriomlem  10340  smobeth  10484  fpwwe2lem5  10533  fpwwe2lem6  10534  fpwwe2lem11  10539  fpwwe2lem12  10540  fpwwe2  10541  axrnegex  11060  axpre-sup  11067  zre  12479  ixxss1  13265  ixxss2  13266  ixxss12  13267  lbioo  13278  ubioo  13279  iccss2  13319  rge0ssre  13358  elfzuz  13422  0wrd0  14449  01sqrexlem6  15156  rlimf  15410  lo1f  15427  lo1dm  15428  o1f  15438  o1dm  15439  mertenslem2  15794  divalglem9  16314  bitsinv2  16356  bitsf1ocnv  16357  gcdcllem1  16412  coprmproddvdslem  16575  prmnn  16587  prmuz2  16609  phimullem  16692  hashgcdlem  16701  1arith  16841  ramtlecl  16914  0ramcl  16937  firest  17338  acsmre  17560  posprs  18224  tospos  18326  latpos  18346  clatpos  18409  dlatl  18432  pslem  18480  tsrlemax  18494  tsrps  18495  chnwrd  18516  sgrpmgm  18634  mndsgrp  18650  grpmnd  18855  nsgsubg  19072  ghmgrp1  19132  ghmgrp2  19133  gimghm  19178  gagrp  19206  gaset  19207  psgneu  19420  efgredeu  19666  ablgrp  19699  cmnmnd  19711  cyggenod2  19799  cyggrp  19804  dprd2dlem1  19957  dprd2da  19958  ablfac2  20005  simpggrp  20010  ogrpgrp  20039  crngring  20165  dvdsrcl  20285  unitcl  20295  rimrhm  20413  brric2  20423  nzrringOLD  20434  subrgring  20491  subrgrcl  20493  rnghmsubcsetclem1  20548  funcrngcsetcALT  20558  rhmsubcsetclem1  20577  rhmsubcrngclem1  20583  domnnzr  20623  drngring  20653  flddrngd  20658  rng1nfld  20696  srngrhm  20762  ofldfld  20789  ofldlt1  20792  lmimlmhm  21000  lveclmod  21042  2idlelbas  21203  rng2idlsubgsubrng  21207  2idlcpblrng  21210  2idlcpbl  21211  qus1  21213  qusrhm  21215  lpirring  21270  cygznlem1  21505  cygznlem3  21508  ofldchr  21515  lbslinds  21772  assalmod  21799  assaring  21800  gsummatr01lem1  22571  topontop  22829  tpstop  22853  mretopd  23008  neiptoptop  23047  perftop  23072  restfpw  23095  cntop1  23156  cntop2  23157  cnptop1  23158  cnptop2  23159  cnprcl  23161  t1ficld  23243  t0top  23245  t1top  23246  haustop  23247  regtop  23249  nrmtop  23252  cnrmtop  23253  pnrmnrm  23256  cmptop  23311  tgcmp  23317  conndisj  23332  conntop  23333  1stctop  23359  llytop  23388  nllytop  23389  hmeocn  23676  filfbas  23764  ufilfil  23820  flimtop  23881  flimfil  23885  alexsublem  23960  ptcmplem3  23970  tsmsfbas  24044  tsmslem1  24045  tsmsgsum  24055  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  tsmsmhm  24062  tsmsadd  24063  tsmsxplem1  24069  tsmsxplem2  24070  tsmsxp  24071  tlmtmd  24103  tlmlmod  24105  tlmtrg  24106  tvctlm  24113  ressust  24179  uspreg  24189  ucncn  24200  neipcfilu  24211  cuspusp  24215  metxmet  24250  xmstps  24369  msxms  24370  xmsxmet  24372  msmet  24373  nrgngp  24578  nlmngp  24593  nlmlmod  24594  nlmnrg  24595  nvcnlm  24612  nmoi  24644  nghmrcl1  24648  nghmrcl2  24649  nmhmrcl1  24663  nmhmrcl2  24664  qdensere  24685  xrge0gsumle  24750  xrge0tsms  24751  icopnfcnv  24868  cvsclm  25054  cphsscph  25179  cmetmet  25214  cmsms  25276  hlbn  25291  ovolicc2lem5  25450  mblss  25460  mbff  25554  mbfres  25573  i1fmbf  25604  limcmpt  25812  c1liplem1  25929  c1lip2  25931  fta1glem1  26101  fta1glem2  26102  fta1g  26103  fta1b  26105  idomrootle  26106  ply1pid  26116  aacn  26253  ulmf2  26321  logdmnrp  26578  logdmss  26579  logcnlem2  26580  logcnlem3  26581  logcnlem4  26582  logcnlem5  26583  logcn  26584  dvloglem  26585  logf1o2  26587  efopnlem1  26593  logtayl2  26599  cxpcn  26682  cxpcnOLD  26683  cxpcn3lem  26685  cxpcn3  26686  resqrtcn  26687  atandmneg  26844  atandmcj  26847  cosatan  26859  cosatanne0  26860  birthdaylem1  26889  areacl  26900  cxp2lim  26915  jensenlem2  26926  jensen  26927  sqff1o  27120  mpodvdsmulf1o  27132  dvdsmulf1o  27134  lgsqrlem1  27285  lgsqrlem2  27286  lgsqrlem3  27287  lgsqrlem4  27288  lgseisenlem3  27316  chebbnd1  27411  chtppilim  27414  chpchtlim  27418  chpo1ub  27419  dchrmusumlema  27432  dchrvmasumiflem1  27440  dchrisum0lema  27453  dchrisum0lem2  27457  selberg3lem2  27497  pntrsumo1  27504  selbergsb  27514  pnt2  27552  sltres  27602  noseponlem  27604  tglineeltr  28610  axcontlem2  28945  axcontlem7  28950  axcontlem8  28951  uhgr0vb  29052  lfuhgr1v0e  29234  fusgrusgr  29302  uvtxisvtx  29369  nbupgruvtxres  29387  cusgrusgr  29399  trliswlk  29676  clwlkiswlk  29754  clwwlkclwwlkn  30012  eupthistrl  30193  frgrusgr  30243  frgrwopreglem5  30303  clwwnonrepclwwnon  30327  ablogrpo  30529  bnnv  30848  hlobn  30870  hcauseq  31167  hlimseqi  31171  hlimveci  31172  shss  31192  sh0  31198  chsh  31206  lnopf  31841  bdopln  31843  hmopf  31856  lnfnf  31866  unopf1o  31898  elunop2  31995  elpjhmop  32167  stcltrlem1  32258  mdslle1i  32299  mdslle2i  32300  2reu2rex1  32462  2reureurex  32463  ssnnssfz  32774  xrge0tsmsd  33049  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  isdrng4  33268  reofld  33315  rearchi  33318  quslsm  33377  ufdidom  33514  mplvrpmga  33593  srafldlvec  33619  rgmoddimOLD  33644  extdggt0  33691  fldextid  33693  extdgid  33694  extdgmul  33697  extdg1id  33700  ist0cld  33867  creftop  33880  lmxrge0  33986  qqhrhm  34023  esumpcvgval  34112  dynkin  34201  measssd  34249  elmbfmvol2  34301  omssubadd  34334  sibfinima  34373  eulerpartlemr  34408  eulerpartlemgf  34413  fiblem  34432  domprobmeas  34444  ballotlemscr  34553  ballotlemfg  34560  ballotlemfrc  34561  ballotlemfrceq  34563  ballotlemrinv0  34567  chtvalz  34663  bnj563  34776  bnj658  34784  bnj667  34785  bnj570  34938  bnj938  34970  bnj1001  34992  bnj1006  34993  bnj1049  35007  bnj1121  35018  bnj1173  35035  bnj1177  35039  bnj1245  35047  bnj1311  35057  bnj1321  35060  bnj1388  35066  bnj1398  35067  bnj1415  35071  bnj1417  35074  bnj1421  35075  bnj1442  35082  bnj1452  35085  bnj1489  35089  bnj1312  35091  pthacycspth  35222  pconntop  35290  sconnpconn  35292  cvmcn  35327  cvmliftlem10  35359  sate0fv0  35482  fundmpss  35832  txpss3v  35941  pprodss4v  35947  outsideofcol  36198  fnebas  36409  filnetlem3  36445  bj-nnfe  36796  bj-xpcossxp  37254  bj-rvecmod  37360  pibt2  37482  phpreu  37664  matunitlindflem1  37676  matunitlindflem2  37677  matunitlindf  37678  poimirlem26  37706  itg2addnc  37734  istotbnd3  37831  totbndmet  37832  sstotbnd2  37834  sstotbnd  37835  equivtotbnd  37838  bndmet  37841  totbndbnd  37849  prdstotbnd  37854  smgrpismgmOLD  37922  mndoissmgrpOLD  37928  crngorngo  38060  prrngorngo  38111  divrngpr  38113  xrnss3v  38425  dfxrn2  38429  refressn  38565  antisymressn  38566  symrelim  38675  eqvrelsym  38721  eqvreltr  38723  disjorimxrn  38866  disjim  38899  disjlem14  38916  ollat  39332  omlol  39359  cvlatl  39444  hlomcmcv  39475  2dim  39589  1dimN  39590  lcfl8b  41623  lclkrlem2  41651  lclkrslem1  41656  lclkrslem2  41657  lcfrlem9  41669  mapdval2N  41749  mapdordlem2  41756  mapdrvallem2  41764  idomnnzgmulnz  42246  aks6d1c6lem3  42285  readvrec2  42479  readvrec  42480  readvcot  42482  nacsacs  42826  eldiophelnn0  42881  lnmlmod  43196  lnrring  43229  mncply  43254  idomodle  43308  areaquad  43333  dfno2  43545  harval3  43655  alephiso3  43676  mnurndlem1  44398  nznngen  44433  binomcxplemcvg  44471  2uasbanh  44678  relpf  45067  disjinfi  45313  climxrre  45872  mbfdmssre  46122  stoweidlem14  46136  stoweidlem16  46138  stoweidlem24  46146  stoweidlem51  46173  stoweidlem54  46176  etransclem32  46388  sge0fodjrnlem  46538  pimrecltpos  46830  pimrecltneg  46846  smfaddlem1  46885  smflimsuplem7  46948  ndmafv  47264  dfafv23  47377  dfatcolem  47379  dfatco  47380  evenz  47754  oddz  47755  gbeeven  47878  gbowodd  47879  sclnbgrisvtx  47973  grlimgredgex  48124  ssnn0ssfz  48473  elbigof  48679  digvalnn0  48724  2sphere  48874  mof0  48962  mof0ALT  48964  uobeq2  49526  thincc  49547  termcthin  49602